DEFINITION drop_gen_skip_r()
TYPE =
       ∀c:C
         .∀x:C
           .∀u:T
             .∀h:nat
               .∀d:nat
                 .∀k:K
                   .drop h (S d) x (CHead c k u)
                     →(ex2
                          C
                          λe:C.eq C x (CHead e k (lift h (r k d) u))
                          λe:C.drop h (r k d) e c)
BODY =
Show proof