let empty
    : ∀(a : Type) → List a
    = λ(a : Type) → [] : List a

in  empty