λ(T : Type) → None T