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