λ(T : Type)
→ λ(x : List T)
→ λ(y : List T)
→ ([] : List T) # x # (([] : List T) # y)