DEFINITION drop_ctail()
TYPE =
       ∀c1:C
         .∀c2:C
           .∀d:nat.∀h:nat.(drop h d c1 c2)→∀k:K.∀u:T.(drop h d (CTail k u c1) (CTail k u c2))
BODY =
Show proof