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