INDUCTIVE DEFINITION pr1 () [ ]
OF ARITY T→T→Prop
BUILT FROM:
     pr1_refl: ∀t:T.(pr1 t t)
   | pr1_sing: ∀t2:T.∀t1:T.(pr0 t1 t2)→∀t3:T.(pr1 t2 t3)→(pr1 t1 t3)