DEFINITION lifts1_cons()
TYPE =
       ∀h:nat
         .∀d:nat
           .∀hds:PList
             .∀ts:TList.(eq TList (lifts1 (PCons h d hds) ts) (lifts h d (lifts1 hds ts)))
BODY =
Show proof