DEFINITION lifts1()
TYPE =
       PList→TList→TList
BODY =
Show proof