DEFINITION lifts()
TYPE =
       nat→nat→TList→TList
BODY =
Show proof