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