∀(x : Type) → x