DEFINITION pc3_ind_left__pc3_pc3_left()
TYPE =
       c:C.t1:T.t2:T.(pc3_left c t1 t2)(pc3 c t1 t2)
BODY =
        assume cC
        assume t1T
        assume t2T
        suppose Hpc3_left c t1 t2
          we proceed by induction on H to prove pc3 c t1 t2
             case pc3_left_r : t:T 
                the thesis becomes pc3 c t t
                   by (pc3_refl . .)
pc3 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 c t0 t4
                (H2) by induction hypothesis we know pc3 c t3 t4
                   by (pc3_pr2_r . . . H0)
                   we proved pc3 c t0 t3
                   by (pc3_t . . . previous . H2)
pc3 c t0 t4
             case pc3_left_ux : t0:T t3:T H0:pr2 c t0 t3 t4:T :pc3_left c t0 t4 
                the thesis becomes pc3 c t3 t4
                (H2) by induction hypothesis we know pc3 c t0 t4
                   by (pc3_pr2_x . . . H0)
                   we proved pc3 c t3 t0
                   by (pc3_t . . . previous . H2)
pc3 c t3 t4
          we proved pc3 c t1 t2
       we proved c:C.t1:T.t2:T.(pc3_left c t1 t2)(pc3 c t1 t2)