fact: Definition wf_solve (wpb : well_formed_matching_problem) := match wpb with | W pb w => build_well_formed_matching_problem_list (solve pb) (well_formed_solve pb w) end.
imports: Coq(Arith List Wellfounded Wf_nat) CoLoR(more_list list_permut list_sort term_spec term_o equational_theory ac matching dickson matching_well_formed matching_well_founded matching_sound matching_complete dickson)