fact: Definition wf_solve_loop : forall (l : list well_formed_matching_problem), (list well_formed_matching_problem) := Fix well_founded_o_lpb (fun l => list well_formed_matching_problem) F_wf_solve.
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)