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