proposition: Theorem red_cb : forall (L : list poly) (p : poly), In p (red L) -> cb L p.
proof: Proof. unfold red in |- *. intros L p H'. generalize (redacc_cb L nil); simpl in |- *; auto. rewrite app_nil_r; auto. Qed.
imports: Coq(List Relation_Definitions) Buchberger(LetP)