proposition: Theorem Cb_incl : forall (a : poly A0 eqA ltM) (P Q : list (poly A0 eqA ltM)), (forall a : poly A0 eqA ltM, In a P -> In a Q) -> Cb a P -> Cb a Q.
proof: Proof. Proof using os minusA invA divA cs A1. intros a; case a; simpl in |- *; auto. intros x H' P Q H'0 H'1. apply CombLinear_incl with (1 := cs) (P := P); auto. intros a0 H'2. apply Incl_inp_inPolySet with (P := P); auto. Qed.
imports: Buchberger(moreCoefStructure)