DEFINITION pc3_ind_left__pc3_left_sym()
TYPE =
       ∀c:C.∀t1:T.∀t2:T.(pc3_left c t1 t2)→(pc3_left c t2 t1)
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 pc3_left c t2 t1
             case pc3_left_r : t:T ⇒
                the thesis becomes pc3_left c t t
                   by (pc3_left_r . .)
pc3_left c t t
             case pc3_left_ur : t0:T t3:T H0:pr2 c t0 t3 t4:T :pc3_left c t3 t4 ⇒
                the thesis becomes pc3_left c t4 t0
                (H2) by induction hypothesis we know pc3_left c t4 t3
                   by (pc3_left_r . .)
                   we proved pc3_left c t0 t0
                   by (pc3_left_ux . . . H0 . previous)
                   we proved pc3_left c t3 t0
                   by (pc3_ind_left__pc3_left_trans . . . H2 . previous)
pc3_left c t4 t0
             case pc3_left_ux : t0:T t3:T H0:pr2 c t0 t3 t4:T :pc3_left c t0 t4 ⇒
                the thesis becomes pc3_left c t4 t3
                (H2) by induction hypothesis we know pc3_left c t4 t0
                   by (pc3_left_r . .)
                   we proved pc3_left c t3 t3
                   by (pc3_left_ur . . . H0 . previous)
                   we proved pc3_left c t0 t3
                   by (pc3_ind_left__pc3_left_trans . . . H2 . previous)
pc3_left c t4 t3
          we proved pc3_left c t2 t1
       we proved ∀c:C.∀t1:T.∀t2:T.(pc3_left c t1 t2)→(pc3_left c t2 t1)