λ(a : Type) → λ(a : Type) → a@1