DEFINITION getl_drop_conf_ge()
TYPE =
       ∀i:nat
         .∀a:C
           .∀c:C
             .getl i c a
               →∀e:C
                    .∀h:nat
                      .∀d:nat
                        .(drop h d c e)→(le (plus d h) i)→(getl (minus i h) e a)
BODY =
        assume i: nat
        assume a: C
        assume c: C
        suppose H: getl i c a
        assume e: C
        assume h: nat
        assume d: nat
        suppose H0: drop h d c e
        suppose H1: le (plus d h) i
          (H2) 
             by (getl_gen_all . . . H)
ex2 C λe:C.drop i O c e λe:C.clear e a
          end of H2
          we proceed by induction on H2 to prove getl (minus i h) e a
             case ex_intro2 : x:C H3:drop i O c x H4:clear x a ⇒
                the thesis becomes getl (minus i h) e a
                   by (drop_conf_ge . . . H3 . . . H0 H1)
                   we proved drop (minus i h) O e x
                   by (getl_intro . . . . previous H4)
getl (minus i h) e a
          we proved getl (minus i h) e a
       we proved 
          ∀i:nat
            .∀a:C
              .∀c:C
                .getl i c a
                  →∀e:C
                       .∀h:nat
                         .∀d:nat
                           .(drop h d c e)→(le (plus d h) i)→(getl (minus i h) e a)