DEFINITION drop_gen_drop()
TYPE =
       ∀k:K
         .∀c:C
           .∀x:C.∀u:T.∀h:nat.(drop (S h) O (CHead c k u) x)→(drop (r k h) O c x)
BODY =
Show proof