DEFINITION getl_drop_conf_rev()
TYPE =
       ∀j:nat
         .∀e1:C
           .∀e2:C
             .drop j O e1 e2
               →∀b:B
                    .∀c2:C
                      .∀v2:T
                        .∀i:nat
                          .getl i c2 (CHead e2 (Bind b) v2)
                            →ex2 C λc1:C.drop j O c1 c2 λc1:C.drop (S i) j c1 e1
BODY =
        assume j: nat
        assume e1: C
        assume e2: C
        suppose H: drop j O e1 e2
        assume b: B
        assume c2: C
        assume v2: T
        assume i: nat
        suppose H0: getl i c2 (CHead e2 (Bind b) v2)
          by (getl_drop . . . . . H0)
          we proved drop (S i) O c2 e2
          by (drop_conf_rev . . . H . . previous)
          we proved ex2 C λc1:C.drop j O c1 c2 λc1:C.drop (S i) j c1 e1
       we proved 
          ∀j:nat
            .∀e1:C
              .∀e2:C
                .drop j O e1 e2
                  →∀b:B
                       .∀c2:C
                         .∀v2:T
                           .∀i:nat
                             .getl i c2 (CHead e2 (Bind b) v2)
                               →ex2 C λc1:C.drop j O c1 c2 λc1:C.drop (S i) j c1 e1