DEFINITION sc3_lift1()
TYPE =
       ∀g:G
         .∀e:C.∀a:A.∀hds:PList.∀c:C.∀t:T.(sc3 g a e t)→(drop1 hds c e)→(sc3 g a c (lift1 hds t))
BODY =
        assume g: G
        assume e: C
        assume a: A
        assume hds: PList
          we proceed by induction on hds to prove ∀c:C.∀t:T.(sc3 g a e t)→(drop1 hds c e)→(sc3 g a c (lift1 hds t))
             case PNil : ⇒
                the thesis becomes ∀c:C.∀t:T.(sc3 g a e t)→(drop1 PNil c e)→(sc3 g a c (lift1 PNil t))
                    assume c: C
                    assume t: T
                    suppose H: sc3 g a e t
                    suppose H0: drop1 PNil c e
                      (H_y) 
                         by (drop1_gen_pnil . . H0)
eq C c e
                      end of H_y
                      by (eq_ind_r . . . H . H_y)
                      we proved sc3 g a c t
                      that is equivalent to sc3 g a c (lift1 PNil t)
∀c:C.∀t:T.(sc3 g a e t)→(drop1 PNil c e)→(sc3 g a c (lift1 PNil t))
             case PCons : n:nat n0:nat p:PList ⇒
                the thesis becomes ∀c:C.∀t:T.∀H0:(sc3 g a e t).∀H1:(drop1 (PCons n n0 p) c e).(sc3 g a c (lift n n0 (lift1 p t)))
                (H) by induction hypothesis we know ∀c:C.∀t:T.(sc3 g a e t)→(drop1 p c e)→(sc3 g a c (lift1 p t))
                    assume c: C
                    assume t: T
                    suppose H0: sc3 g a e t
                    suppose H1: drop1 (PCons n n0 p) c e
                      (H_x) 
                         by (drop1_gen_pcons . . . . . H1)
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 sc3 g a 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 sc3 g a c (lift n n0 (lift1 p t))
                               by (H . . H0 H4)
                               we proved sc3 g a x (lift1 p t)
                               by (sc3_lift . . . . previous . . . H3)
sc3 g a c (lift n n0 (lift1 p t))
                      we proved sc3 g a c (lift n n0 (lift1 p t))
                      that is equivalent to sc3 g a c (lift1 (PCons n n0 p) t)
∀c:C.∀t:T.∀H0:(sc3 g a e t).∀H1:(drop1 (PCons n n0 p) c e).(sc3 g a c (lift n n0 (lift1 p t)))
          we proved ∀c:C.∀t:T.(sc3 g a e t)→(drop1 hds c e)→(sc3 g a c (lift1 hds t))
       we proved 
          ∀g:G
            .∀e:C.∀a:A.∀hds:PList.∀c:C.∀t:T.(sc3 g a e t)→(drop1 hds c e)→(sc3 g a c (lift1 hds t))