DEFINITION wcpr0_drop()
TYPE =
       ∀c1:C
         .∀c2:C
           .wcpr0 c1 c2
             →∀h:nat
                  .∀e1:C
                    .∀u1:T
                      .∀k:K
                        .drop h O c1 (CHead e1 k u1)
                          →ex3_2 C T λe2:C.λu2:T.drop h O c2 (CHead e2 k u2) λe2:C.λ:T.wcpr0 e1 e2 λ:C.λu2:T.pr0 u1 u2
BODY =
Show proof