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 =
Show proof