fact: Record unification_problem : Type := mk_pb { solved_part : substitution; unsolved_part : list (term * term) }.
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)