proposition: Theorem eqp_inv3r : forall a b p q, eqP (pX a p) (pX b q) -> eqP p q.
proof: Proof. intros a b p q H'; simple inversion H'; auto. unfold pO in H0; inversion H0. rewrite (pX_invr p0 p ma a); auto; rewrite (pX_invr q0 q mb b); auto. Qed.
imports: Coq(Arith Compare_dec)