proposition: Lemma descA_subst : forall a b : listA, b = a -> DescA a -> DescA b.
proof: Proof. intros a b H'; rewrite H'; auto. Qed.
imports: Coq(Lexicographic_Exponentiation Relation_Definitions) Coq(Inverse_Image Inclusion List Relation_Operators) Buchberger(Relation_Operators_compat Monomials) Buchberger(Term CoefStructure OrderStructure)