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 =
Show proof