DEFINITION pr3_ind()
TYPE =
       ∀c:C
         .∀P:T→T→Prop
           .∀t:T.(P t t)
             →(∀t:T.∀t1:T.(pr2 c t1 t)→∀t2:T.(pr3 c t t2)→(P t t2)→(P t1 t2)
                  →∀t:T.∀t1:T.(pr3 c t t1)→(P t t1))
BODY =
        assume c: C
        assume P: T→T→Prop
        suppose H: ∀t:T.(P t t)
        suppose H1: ∀t:T.∀t1:T.(pr2 c t1 t)→∀t2:T.(pr3 c t t2)→(P t t2)→(P t1 t2)
          (aux) by well-founded reasoning we prove ∀t:T.∀t1:T.(pr3 c t t1)→(P t t1)
           assume t: T
           assume t1: T
           suppose H2: pr3 c t t1
             by cases on H2 we prove P t t1
                case pr3_refl t2:T ⇒
                   the thesis becomes P t2 t2
                   by (H .)
P t2 t2
                case pr3_sing t2:T t3:T H3:pr2 c t3 t2 t4:T H4:pr3 c t2 t4 ⇒
                   the thesis becomes P t3 t4
                   by (aux . . H4)
                   we proved P t2 t4
                   by (H1 . . H3 . H4 previous)
P t3 t4
             we proved P t t1
∀t:T.∀t1:T.(pr3 c t t1)→(P t t1)
          done
          consider aux
          we proved ∀t:T.∀t1:T.(pr3 c t t1)→(P t t1)
       we proved 
          ∀c:C
            .∀P:T→T→Prop
              .∀t:T.(P t t)
                →(∀t:T.∀t1:T.(pr2 c t1 t)→∀t2:T.(pr3 c t t2)→(P t t2)→(P t1 t2)
                     →∀t:T.∀t1:T.(pr3 c t t1)→(P t t1))