INDUCTIVE DEFINITION drop () [ ]
OF ARITY nat→nat→C→C→Prop
BUILT FROM:
     drop_refl: ∀c:C.(drop O O c c)
   | drop_drop: ∀k:K
                         .∀h:nat
                           .∀c:C.∀e:C.(drop (r k h) O c e)→∀u:T.(drop (S h) O (CHead c k u) e)
   | drop_skip: ∀k:K
                         .∀h:nat
                           .∀d:nat
                             .∀c:C
                               .∀e:C
                                 .drop h (r k d) c e
                                   →∀u:T.(drop h (S d) (CHead c k (lift h (r k d) u)) (CHead e k u))