DEFINITION drop_clear_O()
TYPE =
       ∀b:B
         .∀c:C
           .∀e1:C
             .∀u:T
               .clear c (CHead e1 (Bind b) u)
                 →∀e2:C.∀i:nat.(drop i O e1 e2)→(drop (S i) O c e2)
BODY =
Show proof