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