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 =
        assume h: nat
        assume d: nat
        assume hds: PList
        assume ts: TList
          we proceed by induction on ts to prove eq TList (lifts1 (PCons h d hds) ts) (lifts h d (lifts1 hds ts))
             case TNil : ⇒
                the thesis becomes eq TList (lifts1 (PCons h d hds) TNil) (lifts h d (lifts1 hds TNil))
                   by (refl_equal . .)
                   we proved eq TList TNil TNil
eq TList (lifts1 (PCons h d hds) TNil) (lifts h d (lifts1 hds TNil))
             case TCons : t:T t0:TList ⇒
                the thesis becomes 
                eq
                  TList
                  lifts1 (PCons h d hds) (TCons t t0)
                  lifts h d (lifts1 hds (TCons t t0))
                (H) by induction hypothesis we know eq TList (lifts1 (PCons h d hds) t0) (lifts h d (lifts1 hds t0))
                   by (refl_equal . .)
                   we proved 
                      eq
                        TList
                        TCons (lift h d (lift1 hds t)) (lifts h d (lifts1 hds t0))
                        TCons (lift h d (lift1 hds t)) (lifts h d (lifts1 hds t0))
                   by (eq_ind_r . . . previous . H)
                   we proved 
                      eq
                        TList
                        TCons (lift h d (lift1 hds t)) (lifts1 (PCons h d hds) t0)
                        TCons (lift h d (lift1 hds t)) (lifts h d (lifts1 hds t0))

                      eq
                        TList
                        lifts1 (PCons h d hds) (TCons t t0)
                        lifts h d (lifts1 hds (TCons t t0))
          we proved eq TList (lifts1 (PCons h d hds) ts) (lifts h d (lifts1 hds ts))
       we proved 
          ∀h:nat
            .∀d:nat
              .∀hds:PList
                .∀ts:TList.(eq TList (lifts1 (PCons h d hds) ts) (lifts h d (lifts1 hds ts)))