proposition: Theorem cb_red : forall (L : list poly) (p : poly), In p L -> cb (red L) p.
proof: Proof. intros L p H'. lapply (cb_redacc L nil p); [ intros H'3; generalize H'3 | idtac ]; simpl in |- *; auto. rewrite app_nil_r; auto. Qed.
imports: Coq(List Relation_Definitions) Buchberger(LetP)