proposition: Theorem multTerm_eqT : forall a b c d : Term, eqT a b -> eqT c d -> eqT (multTerm a c) (multTerm b d).
proof: Proof. intros a b c d; case a; case b; case c; case d; unfold eqT in |- *; simpl in |- *; auto. intros H' c0 H'0 c2 H'1 c3 H'2 c4 H'3 H'4; rewrite H'3; rewrite H'4; auto. Qed.
imports: Coq(Relation_Definitions) Buchberger(CoefStructure moreCoefStructure) Buchberger(OrderStructure Monomials)