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