proposition: Theorem wf_Tl : well_founded Tl.
proof: Proof. apply (wf_inverse_image _ _ lt (length (A:=poly A0 eqA ltM))); auto. generalize lt_wf; auto. Qed.
imports: Coq(Arith Inclusion Inverse_Image Wf_nat Relation_Definitions) Coq(Relation_Operators Lexicographic_Product) Buchberger(Relation_Operators_compat LetP)