DEFINITION lifts1_nil()
TYPE =
       ∀ts:TList.(eq TList (lifts1 PNil ts) ts)
BODY =
Show proof