proposition: Theorem addEnd_id2 : forall (a b : poly A0 eqA ltM) (aL : list (poly A0 eqA ltM)), In a aL -> In a (addEnd b aL).
proof: Proof. intros a b aL; elim aL; simpl in |- *; auto. intros a0 l H' H'0; case H'0; auto. Qed.
imports: Buchberger(moreCoefStructure)