DEFINITION wcpr0_gen_head()
TYPE =
       ∀k:K
         .∀c1:C
           .∀x:C
             .∀u1:T
               .wcpr0 (CHead c1 k u1) x
                 →or (eq C x (CHead c1 k u1)) (ex3_2 C T λc2:C.λu2:T.eq C x (CHead c2 k u2) λc2:C.λ:T.wcpr0 c1 c2 λ:C.λu2:T.pr0 u1 u2)
BODY =
Show proof