proposition: Theorem olist_pX_eqT : forall a b p, olist (pX a p) -> eqT a b -> olist (pX b p).
proof: Proof. unfold olist, eqT in |- *. simpl in |- *; auto. intros a b p H' H'0; rewrite <- H'0; auto. Qed.
imports: Coq(Lexicographic_Exponentiation Relation_Definitions) Coq(Inverse_Image Inclusion List Relation_Operators) Buchberger(Relation_Operators_compat Monomials) Buchberger(Term CoefStructure OrderStructure)