proposition: Lemma wf_solve_nil : wf_solve_loop nil = nil.
proof: Proof. rewrite wf_solve_loop_unfold; simpl; 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)