DEFINITION pc3_left_ind()
TYPE =
       ∀c:C
         .∀P:T→T→Prop
           .∀t:T.(P t t)
             →(∀t:T.∀t1:T.(pr2 c t t1)→∀t2:T.(pc3_left c t1 t2)→(P t1 t2)→(P t t2)
                  →(∀t:T.∀t1:T.(pr2 c t t1)→∀t2:T.(pc3_left c t t2)→(P t t2)→(P t1 t2)
                       →∀t:T.∀t1:T.(pc3_left 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 t t1)→∀t2:T.(pc3_left c t1 t2)→(P t1 t2)→(P t t2)
        suppose H2: ∀t:T.∀t1:T.(pr2 c t t1)→∀t2:T.(pc3_left c t t2)→(P t t2)→(P t1 t2)
          (aux) by well-founded reasoning we prove ∀t:T.∀t1:T.(pc3_left c t t1)→(P t t1)
           assume t: T
           assume t1: T
           suppose H3: pc3_left c t t1
             by cases on H3 we prove P t t1
                case pc3_left_r t2:T ⇒
                   the thesis becomes P t2 t2
                   by (H .)
P t2 t2
                case pc3_left_ur t2:T t3:T H4:pr2 c t2 t3 t4:T H5:pc3_left c t3 t4 ⇒
                   the thesis becomes P t2 t4
                   by (aux . . H5)
                   we proved P t3 t4
                   by (H1 . . H4 . H5 previous)
P t2 t4
                case pc3_left_ux t2:T t3:T H4:pr2 c t2 t3 t4:T H5:pc3_left c t2 t4 ⇒
                   the thesis becomes P t3 t4
                   by (aux . . H5)
                   we proved P t2 t4
                   by (H2 . . H4 . H5 previous)
P t3 t4
             we proved P t t1
∀t:T.∀t1:T.(pc3_left c t t1)→(P t t1)
          done
          consider aux
          we proved ∀t:T.∀t1:T.(pc3_left 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 t t1)→∀t2:T.(pc3_left c t1 t2)→(P t1 t2)→(P t t2)
                     →(∀t:T.∀t1:T.(pr2 c t t1)→∀t2:T.(pc3_left c t t2)→(P t t2)→(P t1 t2)
                          →∀t:T.∀t1:T.(pc3_left c t t1)→(P t t1)))