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