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