λ(T : Type) → [] : List T