DEFINITION pr1_ind()
TYPE =
       ∀P:T→T→Prop
         .∀t:T.(P t t)
           →(∀t:T.∀t1:T.(pr0 t1 t)→∀t2:T.(pr1 t t2)→(P t t2)→(P t1 t2)
                →∀t:T.∀t1:T.(pr1 t t1)→(P t t1))
BODY =
        assume P: T→T→Prop
        suppose H: ∀t:T.(P t t)
        suppose H1: ∀t:T.∀t1:T.(pr0 t1 t)→∀t2:T.(pr1 t t2)→(P t t2)→(P t1 t2)
          (aux) by well-founded reasoning we prove ∀t:T.∀t1:T.(pr1 t t1)→(P t t1)
           assume t: T
           assume t1: T
           suppose H2: pr1 t t1
             by cases on H2 we prove P t t1
                case pr1_refl t2:T ⇒
                   the thesis becomes P t2 t2
                   by (H .)
P t2 t2
                case pr1_sing t2:T t3:T H3:pr0 t3 t2 t4:T H4:pr1 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.(pr1 t t1)→(P t t1)
          done
          consider aux
          we proved ∀t:T.∀t1:T.(pr1 t t1)→(P t t1)
       we proved 
          ∀P:T→T→Prop
            .∀t:T.(P t t)
              →(∀t:T.∀t1:T.(pr0 t1 t)→∀t2:T.(pr1 t t2)→(P t t2)→(P t1 t2)
                   →∀t:T.∀t1:T.(pr1 t t1)→(P t t1))