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