INDUCTIVE DEFINITION pr3 () [ :C ]
OF ARITY T→T→Prop
BUILT FROM:
     pr3_refl: ∀t:T.(pr3 c t t)
   | pr3_sing: ∀t2:T.∀t1:T.(pr2 c t1 t2)→∀t3:T.(pr3 c t2 t3)→(pr3 c t1 t3)