DEFINITION lift1_lift1()
TYPE =
       ∀is1:PList.∀is2:PList.∀t:T.(eq T (lift1 is1 (lift1 is2 t)) (lift1 (papp is1 is2) t))
BODY =
       assume is1: PList
          we proceed by induction on is1 to prove ∀is2:PList.∀t:T.(eq T (lift1 is1 (lift1 is2 t)) (lift1 (papp is1 is2) t))
             case PNil : ⇒
                the thesis becomes ∀is2:PList.∀t:T.(eq T (lift1 PNil (lift1 is2 t)) (lift1 (papp PNil is2) t))
                    assume is2: PList
                    assume t: T
                      by (refl_equal . .)
                      we proved eq T (lift1 is2 t) (lift1 is2 t)
                      that is equivalent to eq T (lift1 PNil (lift1 is2 t)) (lift1 (papp PNil is2) t)
∀is2:PList.∀t:T.(eq T (lift1 PNil (lift1 is2 t)) (lift1 (papp PNil is2) t))
             case PCons : n:nat n0:nat p:PList ⇒
                the thesis becomes ∀is2:PList.∀t:T.(eq T (lift n n0 (lift1 p (lift1 is2 t))) (lift n n0 (lift1 (papp p is2) t)))
                (H) by induction hypothesis we know ∀is2:PList.∀t:T.(eq T (lift1 p (lift1 is2 t)) (lift1 (papp p is2) t))
                    assume is2: PList
                    assume t: T
                      (h1) 
                         by (refl_equal . .)
eq nat n n
                      end of h1
                      (h2) 
                         by (refl_equal . .)
eq nat n0 n0
                      end of h2
                      (h3) 
                         by (H . .)
eq T (lift1 p (lift1 is2 t)) (lift1 (papp p is2) t)
                      end of h3
                      by (f_equal3 . . . . . . . . . . . h1 h2 h3)
                      we proved eq T (lift n n0 (lift1 p (lift1 is2 t))) (lift n n0 (lift1 (papp p is2) t))
                      that is equivalent to eq T (lift1 (PCons n n0 p) (lift1 is2 t)) (lift1 (papp (PCons n n0 p) is2) t)
∀is2:PList.∀t:T.(eq T (lift n n0 (lift1 p (lift1 is2 t))) (lift n n0 (lift1 (papp p is2) t)))
          we proved ∀is2:PList.∀t:T.(eq T (lift1 is1 (lift1 is2 t)) (lift1 (papp is1 is2) t))
       we proved ∀is1:PList.∀is2:PList.∀t:T.(eq T (lift1 is1 (lift1 is2 t)) (lift1 (papp is1 is2) t))