DEFINITION lift1_cons_tail()
TYPE =
       ∀t:T
         .∀h:nat
           .∀d:nat.∀hds:PList.(eq T (lift1 (PConsTail hds h d) t) (lift1 hds (lift h d t)))
BODY =
        assume t: T
        assume h: nat
        assume d: nat
        assume hds: PList
          we proceed by induction on hds to prove eq T (lift1 (PConsTail hds h d) t) (lift1 hds (lift h d t))
             case PNil : ⇒
                the thesis becomes eq T (lift1 (PConsTail PNil h d) t) (lift1 PNil (lift h d t))
                   by (refl_equal . .)
                   we proved eq T (lift h d t) (lift h d t)
eq T (lift1 (PConsTail PNil h d) t) (lift1 PNil (lift h d t))
             case PCons : n:nat n0:nat p:PList ⇒
                the thesis becomes 
                eq
                  T
                  lift1 (PConsTail (PCons n n0 p) h d) t
                  lift1 (PCons n n0 p) (lift h d t)
                (H) by induction hypothesis we know eq T (lift1 (PConsTail p h d) t) (lift1 p (lift h d t))
                   by (refl_equal . .)
                   we proved eq T (lift n n0 (lift1 p (lift h d t))) (lift n n0 (lift1 p (lift h d t)))
                   by (eq_ind_r . . . previous . H)
                   we proved 
                      eq T (lift n n0 (lift1 (PConsTail p h d) t)) (lift n n0 (lift1 p (lift h d t)))

                      eq
                        T
                        lift1 (PConsTail (PCons n n0 p) h d) t
                        lift1 (PCons n n0 p) (lift h d t)
          we proved eq T (lift1 (PConsTail hds h d) t) (lift1 hds (lift h d t))
       we proved 
          ∀t:T
            .∀h:nat
              .∀d:nat.∀hds:PList.(eq T (lift1 (PConsTail hds h d) t) (lift1 hds (lift h d t)))