proposition: Lemma wf_solve_loop_unfold : forall l : list well_formed_matching_problem, wf_solve_loop l = @F_wf_solve l (fun y _ => wf_solve_loop y).
proof: Proof. intros; unfold wf_solve_loop; apply Fix_eq with (P:= (fun _:list well_formed_matching_problem => list well_formed_matching_problem)); intros; destruct x. trivial. unfold F_wf_solve; destruct w as [pb w]; destruct pb as [starting_vars un_slvd_part slvd_part party_slvd_part]; destruct un_slvd_part; rewrite H; trivial. Qed.
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)