DEFINITION pc3_ind_left__pc3_left_trans()
TYPE =
       ∀c:C.∀t1:T.∀t2:T.(pc3_left c t1 t2)→∀t3:T.(pc3_left c t2 t3)→(pc3_left c t1 t3)
BODY =
        assume c: C
        assume t1: T
        assume t2: T
        suppose H: pc3_left c t1 t2
          we proceed by induction on H to prove ∀t3:T.(pc3_left c t2 t3)→(pc3_left c t1 t3)
             case pc3_left_r : t:T ⇒
                    assume t3: T
                    suppose H0: pc3_left c t t3
                      consider H0
             case pc3_left_ur : t0:T t3:T H0:pr2 c t0 t3 t4:T :pc3_left c t3 t4 ⇒
                the thesis becomes ∀t5:T.∀H3:(pc3_left c t4 t5).(pc3_left c t0 t5)
                (H2) by induction hypothesis we know ∀t5:T.(pc3_left c t4 t5)→(pc3_left c t3 t5)
                    assume t5: T
                    suppose H3: pc3_left c t4 t5
                      by (H2 . H3)
                      we proved pc3_left c t3 t5
                      by (pc3_left_ur . . . H0 . previous)
                      we proved pc3_left c t0 t5
∀t5:T.∀H3:(pc3_left c t4 t5).(pc3_left c t0 t5)
             case pc3_left_ux : t0:T t3:T H0:pr2 c t0 t3 t4:T :pc3_left c t0 t4 ⇒
                the thesis becomes ∀t5:T.∀H3:(pc3_left c t4 t5).(pc3_left c t3 t5)
                (H2) by induction hypothesis we know ∀t5:T.(pc3_left c t4 t5)→(pc3_left c t0 t5)
                    assume t5: T
                    suppose H3: pc3_left c t4 t5
                      by (H2 . H3)
                      we proved pc3_left c t0 t5
                      by (pc3_left_ux . . . H0 . previous)
                      we proved pc3_left c t3 t5
∀t5:T.∀H3:(pc3_left c t4 t5).(pc3_left c t3 t5)
          we proved ∀t3:T.(pc3_left c t2 t3)→(pc3_left c t1 t3)
       we proved ∀c:C.∀t1:T.∀t2:T.(pc3_left c t1 t2)→∀t3:T.(pc3_left c t2 t3)→(pc3_left c t1 t3)