DEFINITION getl_conf_ge_drop()
TYPE =
       ∀b:B
         .∀c1:C
           .∀e:C
             .∀u:T
               .∀i:nat
                 .getl i c1 (CHead e (Bind b) u)
                   →∀c2:C.(drop (S O) i c1 c2)→(drop i O c2 e)
BODY =
Show proof