proposition: Theorem redInclP : forall (P Q R : list (poly A0 eqA ltM)) (a b : poly A0 eqA ltM), redIn a b P Q R -> forall P1 : list (poly A0 eqA ltM), incl P P1 -> redIn a b P1 Q R.
proof: Proof. intros P Q R a b H'; elim H'; auto. intros P0 Q0 R0 a0 b0 H'0 H'1 P1 H'2. apply redIn0b; auto. intros P0 Q0 R0 a0 b0 c H'0 H'1 H'2 H'3 H'4 H'5 Q1 H'6. apply redIn2 with (c := c); auto. Qed.
imports: Coq(Arith Inclusion Inverse_Image Wf_nat Relation_Definitions) Coq(Relation_Operators Lexicographic_Product) Buchberger(Relation_Operators_compat LetP)