"∀(a : Type) → a"