DEFINITION getl_drop()
TYPE =
       ∀b:B
         .∀c:C
           .∀e:C.∀u:T.∀h:nat.(getl h c (CHead e (Bind b) u))→(drop (S h) O c e)
BODY =
Show proof