∀(t : Type) → ∀(t : t) → < t : t@1 >