fact: Fixpoint extract_solution (solved_part : substitution) (partly_solved_part : list (variable* partly_solved_term)) {struct partly_solved_part} : substitution := match partly_solved_part with | nil => solved_part | (x,x_part_val) :: tl_partly_solved_part => let f := head_symb x_part_val in let x_val := Term f (quicksort (flatten f ((apply_cf_subst solved_part (Var (new_var x_part_val))) :: (closed_term x_part_val) :: nil))) in extract_solution ((x, x_val) :: solved_part) tl_partly_solved_part 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)