DEFINITION pc3_ind_left()
TYPE =
       ∀c:C
         .∀P:T→T→Prop
           .∀t:T.(P t t)
             →(∀t1:T.∀t2:T.(pr2 c t1 t2)→∀t3:T.(pc3 c t2 t3)→(P t2 t3)→(P t1 t3)
                  →(∀t1:T.∀t2:T.(pr2 c t1 t2)→∀t3:T.(pc3 c t1 t3)→(P t1 t3)→(P t2 t3)
                       →∀t:T.∀t0:T.(pc3 c t t0)→(P t t0)))
BODY =
        assume c: C
        assume P: T→T→Prop
        suppose H: ∀t:T.(P t t)
        suppose H0: ∀t1:T.∀t2:T.(pr2 c t1 t2)→∀t3:T.(pc3 c t2 t3)→(P t2 t3)→(P t1 t3)
        suppose H1: ∀t1:T.∀t2:T.(pr2 c t1 t2)→∀t3:T.(pc3 c t1 t3)→(P t1 t3)→(P t2 t3)
        assume t: T
        assume t0: T
        suppose H2: pc3 c t t0
          by (pc3_ind_left__pc3_left_pc3 . . . H2)
          we proved pc3_left c t t0
          we proceed by induction on the previous result to prove P t t0
             case pc3_left_r ⇒
                the thesis becomes the hypothesis H
             case pc3_left_ur : t1:T t2:T H3:pr2 c t1 t2 t3:T H4:pc3_left c t2 t3 ⇒
                the thesis becomes P t1 t3
                (H5) by induction hypothesis we know P t2 t3
                   by (pc3_ind_left__pc3_pc3_left . . . H4)
                   we proved pc3 c t2 t3
                   by (H0 . . H3 . previous H5)
P t1 t3
             case pc3_left_ux : t1:T t2:T H3:pr2 c t1 t2 t3:T H4:pc3_left c t1 t3 ⇒
                the thesis becomes P t2 t3
                (H5) by induction hypothesis we know P t1 t3
                   by (pc3_ind_left__pc3_pc3_left . . . H4)
                   we proved pc3 c t1 t3
                   by (H1 . . H3 . previous H5)
P t2 t3
          we proved P t t0
       we proved 
          ∀c:C
            .∀P:T→T→Prop
              .∀t:T.(P t t)
                →(∀t1:T.∀t2:T.(pr2 c t1 t2)→∀t3:T.(pc3 c t2 t3)→(P t2 t3)→(P t1 t3)
                     →(∀t1:T.∀t2:T.(pr2 c t1 t2)→∀t3:T.(pc3 c t1 t3)→(P t1 t3)→(P t2 t3)
                          →∀t:T.∀t0:T.(pc3 c t t0)→(P t t0)))