DEFINITION lift1()
TYPE =
PList
→
T
→
T
BODY =
Show proof