DEFINITION drop_getl_trans_le()
TYPE =
       ∀i:nat
         .∀d:nat
           .le i d
             →∀c1:C
                  .∀c2:C
                    .∀h:nat
                      .drop h d c1 c2
                        →∀e2:C
                             .getl i c2 e2
                               →ex3_2 C C λe0:C.λ:C.drop i O c1 e0 λe0:C.λe1:C.drop h (minus d i) e0 e1 λ:C.λe1:C.clear e1 e2
BODY =
        assume i: nat
        assume d: nat
        suppose H: le i d
        assume c1: C
        assume c2: C
        assume h: nat
        suppose H0: drop h d c1 c2
        assume e2: C
        suppose H1: getl i c2 e2
          (H2) 
             by (getl_gen_all . . . H1)
ex2 C λe:C.drop i O c2 e λe:C.clear e e2
          end of H2
          we proceed by induction on H2 to prove ex3_2 C C λe0:C.λ:C.drop i O c1 e0 λe0:C.λe1:C.drop h (minus d i) e0 e1 λ:C.λe1:C.clear e1 e2
             case ex_intro2 : x:C H3:drop i O c2 x H4:clear x e2 ⇒
                the thesis becomes ex3_2 C C λe0:C.λ:C.drop i O c1 e0 λe0:C.λe1:C.drop h (minus d i) e0 e1 λ:C.λe1:C.clear e1 e2
                   (H5) 
                      by (drop_trans_le . . H . . . H0 . H3)
ex2 C λe1:C.drop i O c1 e1 λe1:C.drop h (minus d i) e1 x
                   end of H5
                   we proceed by induction on H5 to prove ex3_2 C C λe0:C.λ:C.drop i O c1 e0 λe0:C.λe1:C.drop h (minus d i) e0 e1 λ:C.λe1:C.clear e1 e2
                      case ex_intro2 : x0:C H6:drop i O c1 x0 H7:drop h (minus d i) x0 x ⇒
                         the thesis becomes ex3_2 C C λe0:C.λ:C.drop i O c1 e0 λe0:C.λe1:C.drop h (minus d i) e0 e1 λ:C.λe1:C.clear e1 e2
                            by (ex3_2_intro . . . . . . . H6 H7 H4)
ex3_2 C C λe0:C.λ:C.drop i O c1 e0 λe0:C.λe1:C.drop h (minus d i) e0 e1 λ:C.λe1:C.clear e1 e2
ex3_2 C C λe0:C.λ:C.drop i O c1 e0 λe0:C.λe1:C.drop h (minus d i) e0 e1 λ:C.λe1:C.clear e1 e2
          we proved ex3_2 C C λe0:C.λ:C.drop i O c1 e0 λe0:C.λe1:C.drop h (minus d i) e0 e1 λ:C.λe1:C.clear e1 e2
       we proved 
          ∀i:nat
            .∀d:nat
              .le i d
                →∀c1:C
                     .∀c2:C
                       .∀h:nat
                         .drop h d c1 c2
                           →∀e2:C
                                .getl i c2 e2
                                  →ex3_2 C C λe0:C.λ:C.drop i O c1 e0 λe0:C.λe1:C.drop h (minus d i) e0 e1 λ:C.λe1:C.clear e1 e2