proposition: Lemma extract_solution_in_solved_part : forall solved_part partly_solved_part v t, nb_occ X.eq_bool v solved_part + nb_occ X.eq_bool v partly_solved_part <= 1 -> find X.eq_bool v solved_part = Some t -> apply_cf_subst (extract_solution solved_part partly_solved_part) (Var v) = t.
proof: Proof. intros sp psp; generalize sp; clear sp; induction psp as [ | [x s] psp]; intros sp v t H v_sp. simpl; rewrite v_sp; trivial. rewrite extract_solution_unfold; apply IHpsp. simpl; simpl in H; revert H; generalize (X.eq_bool_ok v x); case (X.eq_bool v x); [intro v_eq_x | intro v_diff_x]; trivial. intro H; rewrite Nat.add_comm in H; simpl in H; rewrite Nat.add_comm in H; simpl; trivial. revert H; simpl; generalize (X.eq_bool_ok v x); case (X.eq_bool v x); [intros _ | intro v_diff_x]; trivial. generalize (some_nb_occ_Sn X.eq_bool v _ v_sp); destruct (nb_occ X.eq_bool v sp) as [ | n]. intro; absurd (1 <= 0); auto with arith. intros _ H; simpl in H; rewrite Nat.add_comm in H; simpl in H. absurd (S(S (nb_occ X.eq_bool v psp + n)) <= 1); auto with arith. 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)