proposition: Theorem redIn_nil : forall (R : list (poly A0 eqA ltM)) (a b : poly A0 eqA ltM), In a R -> In b R -> redIn a b R nil R -> reds a b R.
proof: Proof. intros R a b H' H'0 H'1. apply lem_redIn_nil with (aP := R) (Q := nil (A:=poly A0 eqA ltM)); auto. Qed.
imports: Coq(Arith Inclusion Inverse_Image Wf_nat Relation_Definitions) Coq(Relation_Operators Lexicographic_Product) Buchberger(Relation_Operators_compat LetP)