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