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