proposition: Lemma extract_solution_unfold : forall solved_part partly_solved_part x x_part_val, extract_solution solved_part ((x,x_part_val) :: partly_solved_part) = extract_solution ((x, (Term (head_symb x_part_val) (quicksort (flatten (head_symb x_part_val) ((apply_cf_subst solved_part (Var (new_var x_part_val))) :: (closed_term x_part_val) :: nil))))) :: solved_part) partly_solved_part.
proof: Proof. intros; 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)