proposition: Lemma wf_solve_loop_end : forall lpb wpb, In wpb (wf_solve_loop lpb) -> match wpb with | W pb _ => (unsolved_part pb) = nil end.
proof: Proof. intro lpb; refine (well_founded_ind well_founded_o_lpb (fun lpb => forall wpb, In wpb (wf_solve_loop lpb) -> match wpb with | W pb _ => (unsolved_part pb) = nil end) _ _). clear lpb; intros lpb IH wpb; destruct lpb. rewrite wf_solve_nil; contradiction. rewrite wf_solve_cons; destruct w. cut (forall pb1, pb1 = pb -> unsolved_part pb1 = unsolved_part pb). intro H; destruct (unsolved_part pb); generalize (H pb (eq_refl _)); clear H; intros H In_wpb. elim In_wpb; clear In_wpb; intro In_wpb. subst wpb; trivial. refine (IH lpb (F_wf_solve_dec1 _ _) _ In_wpb). refine (IH (wf_solve (W pb w) ++ lpb) (F_wf_solve_dec2 _ _) _ In_wpb). intros; subst pb; 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)