DEFINITION sns3_lifts1()
TYPE =
       ∀e:C.∀hds:PList.∀c:C.(drop1 hds c e)→∀ts:TList.(sns3 e ts)→(sns3 c (lifts1 hds ts))
BODY =
        assume e: C
        assume hds: PList
          we proceed by induction on hds to prove ∀c:C.(drop1 hds c e)→∀ts:TList.(sns3 e ts)→(sns3 c (lifts1 hds ts))
             case PNil : ⇒
                the thesis becomes ∀c:C.(drop1 PNil c e)→∀ts:TList.(sns3 e ts)→(sns3 c (lifts1 PNil ts))
                    assume c: C
                    suppose H: drop1 PNil c e
                    assume ts: TList
                    suppose H0: sns3 e ts
                      (H_y) 
                         by (drop1_gen_pnil . . H)
eq C c e
                      end of H_y
                      by (lifts1_nil .)
                      we proved eq TList (lifts1 PNil ts) ts
                      by (eq_ind_r . . . H0 . previous)
                      we proved sns3 e (lifts1 PNil ts)
                      by (eq_ind_r . . . previous . H_y)
                      we proved sns3 c (lifts1 PNil ts)
∀c:C.(drop1 PNil c e)→∀ts:TList.(sns3 e ts)→(sns3 c (lifts1 PNil ts))
             case PCons : n:nat n0:nat p:PList ⇒
                the thesis becomes ∀c:C.∀H0:(drop1 (PCons n n0 p) c e).∀ts:TList.∀H1:(sns3 e ts).(sns3 c (lifts1 (PCons n n0 p) ts))
                (H) by induction hypothesis we know ∀c:C.(drop1 p c e)→∀ts:TList.(sns3 e ts)→(sns3 c (lifts1 p ts))
                    assume c: C
                    suppose H0: drop1 (PCons n n0 p) c e
                    assume ts: TList
                    suppose H1: sns3 e ts
                      (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 sns3 c (lifts1 (PCons n n0 p) ts)
                         case ex_intro2 : x:C H3:drop n n0 c x H4:drop1 p x e ⇒
                            the thesis becomes sns3 c (lifts1 (PCons n n0 p) ts)
                               (h1) 
                                  by (H . H4 . H1)
                                  we proved sns3 x (lifts1 p ts)
                                  by (sns3_lifts . . . . H3 . previous)
sns3 c (lifts n n0 (lifts1 p ts))
                               end of h1
                               (h2) 
                                  by (lifts1_cons . . . .)
eq TList (lifts1 (PCons n n0 p) ts) (lifts n n0 (lifts1 p ts))
                               end of h2
                               by (eq_ind_r . . . h1 . h2)
sns3 c (lifts1 (PCons n n0 p) ts)
                      we proved sns3 c (lifts1 (PCons n n0 p) ts)
∀c:C.∀H0:(drop1 (PCons n n0 p) c e).∀ts:TList.∀H1:(sns3 e ts).(sns3 c (lifts1 (PCons n n0 p) ts))
          we proved ∀c:C.(drop1 hds c e)→∀ts:TList.(sns3 e ts)→(sns3 c (lifts1 hds ts))
       we proved 
          ∀e:C.∀hds:PList.∀c:C.(drop1 hds c e)→∀ts:TList.(sns3 e ts)→(sns3 c (lifts1 hds ts))