DEFINITION drop_getl_trans_ge()
TYPE =
       ∀i:nat
         .∀c1:C
           .∀c2:C
             .∀d:nat
               .∀h:nat
                 .drop h d c1 c2
                   →∀e2:C.(getl i c2 e2)→(le d i)→(getl (plus i h) c1 e2)
BODY =
        assume i: nat
        assume c1: C
        assume c2: C
        assume d: nat
        assume h: nat
        suppose H: drop h d c1 c2
        assume e2: C
        suppose H0: getl i c2 e2
        suppose H1: le d i
          (H2) 
             by (getl_gen_all . . . H0)
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 getl (plus i h) c1 e2
             case ex_intro2 : x:C H3:drop i O c2 x H4:clear x e2 ⇒
                the thesis becomes getl (plus i h) c1 e2
                   by (drop_trans_ge . . . . . H . H3 H1)
                   we proved drop (plus i h) O c1 x
                   by (getl_intro . . . . previous H4)
getl (plus i h) c1 e2
          we proved getl (plus i h) c1 e2
       we proved 
          ∀i:nat
            .∀c1:C
              .∀c2:C
                .∀d:nat
                  .∀h:nat
                    .drop h d c1 c2
                      →∀e2:C.(getl i c2 e2)→(le d i)→(getl (plus i h) c1 e2)