DEFINITION getl_drop_trans()
TYPE =
       ∀c1:C
         .∀c2:C
           .∀h:nat
             .getl h c1 c2
               →∀e2:C.∀i:nat.(drop (S i) O c2 e2)→(drop (S (plus i h)) O c1 e2)
BODY =
Show proof