DEFINITION lift1_xhg()
TYPE =
       ∀hds:PList
         .∀t:T.(eq T (lift1 (Ss hds) (lift (S O) O t)) (lift (S O) O (lift1 hds t)))
BODY =
Show proof