λ(T : Type) → [] : List { index : Natural, value : T }