to serve as base for the order relations: p < q and p ≤ q *)
inductive pprec: relation ptr ≝
| pprec_nil : ∀c,q. pprec (◊) (c::q)
to serve as base for the order relations: p < q and p ≤ q *)
inductive pprec: relation ptr ≝
| pprec_nil : ∀c,q. pprec (◊) (c::q)