proposition: Theorem cb_red_cb1 : forall (p : poly) (L : list poly), cb L p -> cb (red L) p.
proof: Proof. intros p L H'. apply cb_compo with (L1 := L); auto. intros q H'0. apply cb_red; auto. Qed.
imports: Coq(List Relation_Definitions) Buchberger(LetP)