DEFINITION lifts1_xhg()
TYPE =
       ∀hds:PList
         .∀ts:TList
           .eq
             TList
             lifts1 (Ss hds) (lifts (S O) O ts)
             lifts (S O) O (lifts1 hds ts)
BODY =
Show proof