fact: Definition matching t1 t2 Wt1 Wt2 := map (fun wpb => match wpb with | W pb _ => clean_sol (existential_vars pb) (extract_solution (solved_part pb) (partly_solved_part pb)) end) (wf_solve_loop ((W (init_pb t1 t2) (well_formed_init_pb t1 t2 Wt1 Wt2)) :: nil)).
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)