proposition: Theorem wf_Fl : forall x : list (poly A0 eqA ltM), well_founded (Fl x).
proof: Proof. unfold FPset in |- *; simpl in |- *. intros x; generalize wf_Tl; auto. Qed.
imports: Coq(Arith Inclusion Inverse_Image Wf_nat Relation_Definitions) Coq(Relation_Operators Lexicographic_Product) Buchberger(Relation_Operators_compat LetP)