DEFINITION lifts_inj()
TYPE =
       ∀xs:TList
         .∀ts:TList
           .∀h:nat
             .∀d:nat
               .(eq TList (lifts h d xs) (lifts h d ts))→(eq TList xs ts)
BODY =
Show proof