proposition: Theorem eqTerm_refl : reflexive Term eqTerm.
proof: Proof. Proof using plusA multA minusA invA divA cs A1 A0. red in |- *. intros x; case x; simpl in |- *; auto. Qed.
imports: Coq(Relation_Definitions) Buchberger(CoefStructure moreCoefStructure) Buchberger(OrderStructure Monomials)