proposition: Theorem addEnd_cons : forall (a b : poly A0 eqA ltM) (aL : list (poly A0 eqA ltM)), In a (addEnd b aL) -> a = b \/ In a aL.
proof: Proof. intros a b aL; elim aL; simpl in |- *; auto. intros H'; case H'; [ intros H'0; rewrite <- H'0 | intros H'0; clear H' ]; auto. intros a0 l H' H'0; case H'0; [ intros H'1; rewrite <- H'1; clear H'0 | intros H'1; clear H'0 ]; auto. case (H' H'1); auto. Qed.
imports: Buchberger(moreCoefStructure)