DEFINITION nf2_lift1()
TYPE =
       ∀e:C.∀hds:PList.∀c:C.∀t:T.(drop1 hds c e)→(nf2 e t)→(nf2 c (lift1 hds t))
BODY =
        assume e: C
        assume hds: PList
          we proceed by induction on hds to prove ∀c:C.∀t:T.(drop1 hds c e)→(nf2 e t)→(nf2 c (lift1 hds t))
             case PNil : ⇒
                the thesis becomes ∀c:C.∀t:T.(drop1 PNil c e)→(nf2 e t)→(nf2 c (lift1 PNil t))
                    assume c: C
                    assume t: T
                    suppose H: drop1 PNil c e
                    suppose H0: nf2 e t
                      (H_y) 
                         by (drop1_gen_pnil . . H)
eq C c e
                      end of H_y
                      by (eq_ind_r . . . H0 . H_y)
                      we proved nf2 c t
                      that is equivalent to nf2 c (lift1 PNil t)
∀c:C.∀t:T.(drop1 PNil c e)→(nf2 e t)→(nf2 c (lift1 PNil t))
             case PCons : n:nat n0:nat p:PList ⇒
                the thesis becomes ∀c:C.∀t:T.∀H0:(drop1 (PCons n n0 p) c e).∀H1:(nf2 e t).(nf2 c (lift n n0 (lift1 p t)))
                (H) by induction hypothesis we know ∀c:C.∀t:T.(drop1 p c e)→(nf2 e t)→(nf2 c (lift1 p t))
                    assume c: C
                    assume t: T
                    suppose H0: drop1 (PCons n n0 p) c e
                    suppose H1: nf2 e t
                      (H_x) 
                         by (drop1_gen_pcons . . . . . H0)
ex2 C λc2:C.drop n n0 c c2 λc2:C.drop1 p c2 e
                      end of H_x
                      (H2) consider H_x
                      we proceed by induction on H2 to prove nf2 c (lift n n0 (lift1 p t))
                         case ex_intro2 : x:C H3:drop n n0 c x H4:drop1 p x e ⇒
                            the thesis becomes nf2 c (lift n n0 (lift1 p t))
                               by (H . . H4 H1)
                               we proved nf2 x (lift1 p t)
                               by (nf2_lift . . previous . . . H3)
nf2 c (lift n n0 (lift1 p t))
                      we proved nf2 c (lift n n0 (lift1 p t))
                      that is equivalent to nf2 c (lift1 (PCons n n0 p) t)
∀c:C.∀t:T.∀H0:(drop1 (PCons n n0 p) c e).∀H1:(nf2 e t).(nf2 c (lift n n0 (lift1 p t)))
          we proved ∀c:C.∀t:T.(drop1 hds c e)→(nf2 e t)→(nf2 c (lift1 hds t))
       we proved ∀e:C.∀hds:PList.∀c:C.∀t:T.(drop1 hds c e)→(nf2 e t)→(nf2 c (lift1 hds t))