proposition: Theorem eqTerm_imp_eqT : forall a b : Term, eqTerm a b -> eqT a b.
proof: Proof. intros a b; case a; case b; simpl in |- *; intuition. Qed.
imports: Coq(Relation_Definitions) Buchberger(CoefStructure moreCoefStructure) Buchberger(OrderStructure Monomials)