DEFINITION pc3_left_ind()
TYPE =
       ∀c:C
         .∀P:T→T→Prop
           .∀t:T.(P t t)
             →(∀t:T.∀t1:T.(pr2 c t t1)→∀t2:T.(pc3_left c t1 t2)→(P t1 t2)→(P t t2)
                  →(∀t:T.∀t1:T.(pr2 c t t1)→∀t2:T.(pc3_left c t t2)→(P t t2)→(P t1 t2)
                       →∀t:T.∀t1:T.(pc3_left c t t1)→(P t t1)))
BODY =
Show proof