fact: Record matching_problem : Type := mk_pb { existential_vars : list variable; unsolved_part : list (term * term); solved_part : substitution; partly_solved_part : list (variable * partly_solved_term) }.
imports: Coq(Arith List) CoLoR(more_list list_sort term_spec ac cf_eq_ac)