proposition: Theorem genPcPf_incl : forall (a : poly A0 eqA ltM) (aL Q : list (poly A0 eqA ltM)), incl Q (genPcPf a aL Q).
proof: Proof. intros a aL Q; unfold genPcPf in |- *; case (genPcPf0 a aL Q). intros x H'. apply genPcP_incl with (i := a) (L1 := aL); auto. Qed.
imports: Coq(Arith Inclusion Inverse_Image Wf_nat Relation_Definitions) Coq(Relation_Operators Lexicographic_Product) Buchberger(Relation_Operators_compat LetP)