proposition: Lemma wf_lt_pb : well_founded lt_pb.
proof: Proof. unfold lt_pb; apply (wf_inverse_image unification_problem _ lt_ms measure_for_unif_pb wf_lt_ms). Defined.
imports: Coq(Arith Wf_nat Wellfounded List Multiset Relations) CoLoR(closure decidable_set ordered_set more_list list_permut list_set list_sort dickson term_spec term)