DEFINITION wcpr0_ind()
TYPE =
       ∀P:C→C→Prop
         .∀c:C.(P c c)
           →(∀c:C
                  .∀c1:C
                    .wcpr0 c c1
                      →(P c c1)→∀t:T.∀t1:T.(pr0 t t1)→∀k:K.(P (CHead c k t) (CHead c1 k t1))
                →∀c:C.∀c1:C.(wcpr0 c c1)→(P c c1))
BODY =
Show proof