proposition: Theorem unit_T1 : forall p : poly A0 eqA ltM, eqT (unit p) (T1 A1 n).
proof: Proof. unfold eqT in |- *; intros p; case p. intros x; case x; simpl in |- *; auto. intros a l; case a; simpl in |- *; auto. Qed.
imports: Buchberger(moreCoefStructure)