∀(x : Type) → Type → x