DEFINITION csubc_drop1_conf_rev()
TYPE =
       ∀g:G
         .∀hds:PList
           .∀c2:C.∀e2:C.(drop1 hds c2 e2)→∀e1:C.(csubc g e1 e2)→(ex2 C λc1:C.drop1 hds c1 e1 λc1:C.csubc g c1 c2)
BODY =
        assume g: G
        assume hds: PList
          we proceed by induction on hds to prove ∀c2:C.∀e2:C.(drop1 hds c2 e2)→∀e1:C.(csubc g e1 e2)→(ex2 C λc1:C.drop1 hds c1 e1 λc1:C.csubc g c1 c2)
             case PNil : ⇒
                the thesis becomes ∀c2:C.∀e2:C.(drop1 PNil c2 e2)→∀e1:C.(csubc g e1 e2)→(ex2 C λc1:C.drop1 PNil c1 e1 λc1:C.csubc g c1 c2)
                    assume c2: C
                    assume e2: C
                    suppose H: drop1 PNil c2 e2
                    assume e1: C
                    suppose H0: csubc g e1 e2
                      (H_y) 
                         by (drop1_gen_pnil . . H)
eq C c2 e2
                      end of H_y
                      (H1) 
                         by (eq_ind_r . . . H0 . H_y)
csubc g e1 c2
                      end of H1
                      by (drop1_nil .)
                      we proved drop1 PNil e1 e1
                      by (ex_intro2 . . . . previous H1)
                      we proved ex2 C λc1:C.drop1 PNil c1 e1 λc1:C.csubc g c1 c2
∀c2:C.∀e2:C.(drop1 PNil c2 e2)→∀e1:C.(csubc g e1 e2)→(ex2 C λc1:C.drop1 PNil c1 e1 λc1:C.csubc g c1 c2)
             case PCons : n:nat n0:nat p:PList ⇒
                the thesis becomes ∀c2:C.∀e2:C.∀H0:(drop1 (PCons n n0 p) c2 e2).∀e1:C.∀H1:(csubc g e1 e2).(ex2 C λc1:C.drop1 (PCons n n0 p) c1 e1 λc1:C.csubc g c1 c2)
                (H) by induction hypothesis we know ∀c2:C.∀e2:C.(drop1 p c2 e2)→∀e1:C.(csubc g e1 e2)→(ex2 C λc1:C.drop1 p c1 e1 λc1:C.csubc g c1 c2)
                    assume c2: C
                    assume e2: C
                    suppose H0: drop1 (PCons n n0 p) c2 e2
                    assume e1: C
                    suppose H1: csubc g e1 e2
                      (H_x) 
                         by (drop1_gen_pcons . . . . . H0)
ex2 C λc2:C.drop n n0 c2 c2 λc2:C.drop1 p c2 e2
                      end of H_x
                      (H2) consider H_x
                      we proceed by induction on H2 to prove ex2 C λc1:C.drop1 (PCons n n0 p) c1 e1 λc1:C.csubc g c1 c2
                         case ex_intro2 : x:C H3:drop n n0 c2 x H4:drop1 p x e2 ⇒
                            the thesis becomes ex2 C λc1:C.drop1 (PCons n n0 p) c1 e1 λc1:C.csubc g c1 c2
                               (H_x0) 
                                  by (H . . H4 . H1)
ex2 C λc1:C.drop1 p c1 e1 λc1:C.csubc g c1 x
                               end of H_x0
                               (H5) consider H_x0
                               we proceed by induction on H5 to prove ex2 C λc1:C.drop1 (PCons n n0 p) c1 e1 λc1:C.csubc g c1 c2
                                  case ex_intro2 : x0:C H6:drop1 p x0 e1 H7:csubc g x0 x ⇒
                                     the thesis becomes ex2 C λc1:C.drop1 (PCons n n0 p) c1 e1 λc1:C.csubc g c1 c2
                                        (H_x1) 
                                           by (csubc_drop_conf_rev . . . . . H3 . H7)
ex2 C λc1:C.drop n n0 c1 x0 λc1:C.csubc g c1 c2
                                        end of H_x1
                                        (H8) consider H_x1
                                        we proceed by induction on H8 to prove ex2 C λc1:C.drop1 (PCons n n0 p) c1 e1 λc1:C.csubc g c1 c2
                                           case ex_intro2 : x1:C H9:drop n n0 x1 x0 H10:csubc g x1 c2 ⇒
                                              the thesis becomes ex2 C λc1:C.drop1 (PCons n n0 p) c1 e1 λc1:C.csubc g c1 c2
                                                 by (drop1_cons . . . . H9 . . H6)
                                                 we proved drop1 (PCons n n0 p) x1 e1
                                                 by (ex_intro2 . . . . previous H10)
ex2 C λc1:C.drop1 (PCons n n0 p) c1 e1 λc1:C.csubc g c1 c2
ex2 C λc1:C.drop1 (PCons n n0 p) c1 e1 λc1:C.csubc g c1 c2
ex2 C λc1:C.drop1 (PCons n n0 p) c1 e1 λc1:C.csubc g c1 c2
                      we proved ex2 C λc1:C.drop1 (PCons n n0 p) c1 e1 λc1:C.csubc g c1 c2
∀c2:C.∀e2:C.∀H0:(drop1 (PCons n n0 p) c2 e2).∀e1:C.∀H1:(csubc g e1 e2).(ex2 C λc1:C.drop1 (PCons n n0 p) c1 e1 λc1:C.csubc g c1 c2)
          we proved ∀c2:C.∀e2:C.(drop1 hds c2 e2)→∀e1:C.(csubc g e1 e2)→(ex2 C λc1:C.drop1 hds c1 e1 λc1:C.csubc g c1 c2)
       we proved 
          ∀g:G
            .∀hds:PList
              .∀c2:C.∀e2:C.(drop1 hds c2 e2)→∀e1:C.(csubc g e1 e2)→(ex2 C λc1:C.drop1 hds c1 e1 λc1:C.csubc g c1 c2)