INDUCTIVE DEFINITION pc3_left () [ :C ]
OF ARITY T→T→Prop
BUILT FROM:
     pc3_left_r: ∀t:T.(pc3_left c t t)
   | pc3_left_ur: ∀t1:T.∀t2:T.(pr2 c t1 t2)→∀t3:T.(pc3_left c t2 t3)→(pc3_left c t1 t3)
   | pc3_left_ux: ∀t1:T.∀t2:T.(pr2 c t1 t2)→∀t3:T.(pc3_left c t1 t3)→(pc3_left c t2 t3)