proposition: Lemma wf_solve_cons : forall wpb lpb, wf_solve_loop (wpb :: lpb) = match wpb with | W pb w => match unsolved_part pb with | nil => wpb :: (wf_solve_loop lpb) | _ :: _ => wf_solve_loop ((wf_solve wpb) ++ lpb) end end.
proof: Proof. intros wpb lpb; rewrite wf_solve_loop_unfold; destruct wpb as [pb w]; destruct pb as [starting_vars un_slvd_part slvd_part party_slvd_part]; destruct un_slvd_part; 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)