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 =
        assume P: C→C→Prop
        suppose H: ∀c:C.(P c c)
        suppose H1: 
           ∀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))
          (aux) by well-founded reasoning we prove ∀c:C.∀c1:C.(wcpr0 c c1)→(P c c1)
           assume c: C
           assume c1: C
           suppose H2: wcpr0 c c1
             by cases on H2 we prove P c c1
                case wcpr0_refl c2:C ⇒
                   the thesis becomes P c2 c2
                   by (H .)
P c2 c2
                case wcpr0_comp c2:C c3:C H3:wcpr0 c2 c3 t:T t1:T H4:pr0 t t1 k:K ⇒
                   the thesis becomes P (CHead c2 k t) (CHead c3 k t1)
                   by (aux . . H3)
                   we proved P c2 c3
                   by (H1 . . H3 previous . . H4 .)
P (CHead c2 k t) (CHead c3 k t1)
             we proved P c c1
∀c:C.∀c1:C.(wcpr0 c c1)→(P c c1)
          done
          consider aux
          we proved ∀c:C.∀c1:C.(wcpr0 c c1)→(P c c1)
       we proved 
          ∀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))