λ(a : Type) → ∀(b : a) → a