proposition: Theorem pO_minusP_inv2 : forall p q : list (Term A n), minusP p (pO A n) q -> p = q.
proof: Proof. intros p; elim p. intros q H'; inversion H'; auto. intros a l H' q H'0; inversion H'0; auto. Qed.
imports: Coq(Arith) Buchberger(LetP)