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