proposition: Theorem red_incl : forall (a : poly A0 eqA ltM) (p q : list (poly A0 eqA ltM)), incl p q -> red a p -> red a q.
proof: Proof. Proof using plusA os cs. unfold red in |- *. intros a p q H' H'0. inversion H'0. apply rstar_rtopO; auto. case a; auto. apply inP_reducestar with (Q := p); auto. intros a0 H'1. apply Incl_inp_inPolySet with (P := p); auto. Qed.
imports: Buchberger(moreCoefStructure)