proposition: Lemma eqT_trans : transitive _ eqT.
proof: Proof. red in |- *; unfold eqT in |- *. intros x y z H' H'0; rewrite H'; auto. Qed.
imports: Coq(Relation_Definitions) Buchberger(CoefStructure moreCoefStructure) Buchberger(OrderStructure Monomials)