proposition: Lemma no_var_in_subst_inv : forall z sigma, (forall v v_val, find X.eq_bool v sigma = Some v_val -> var_in_term z v_val = false) -> forall c v v_val, VSet.mem v (domain_of_subst sigma) -> find X.eq_bool v (acc_inst c sigma) = Some v_val -> var_in_term z v_val = false.
proof: Proof. intros z sigma H c; revert z sigma H; induction c as [ | x c]; intros z sigma H v v_val v_in_dom F. simpl in F; apply (H v _ F). simpl in F; refine (IHc _ _ _ _ _ _ F); clear F. intros w w_val F. assert (F' := find_map_subst w x (apply_subst sigma (Var x)) sigma). simpl in F'; case_eq (find X.eq_bool w sigma); [intro w_val' | idtac]; intro w_sigma; rewrite w_sigma in F'. rewrite F in F'; injection F'; clear F F'; intro F'; subst w_val. assert (z_not_in_w_val' := H _ _ w_sigma). case_eq (find X.eq_bool x sigma); [intro x_val | idtac]; intro x_sigma. assert (z_not_in_x_val := H _ _ x_sigma). apply no_var_in_term_inv; trivial. replace (apply_subst ((x, Var x) :: nil) w_val') with (apply_subst nil w_val'). rewrite empty_subst_is_id; trivial. rewrite <- subst_eq_vars. intros y _; simpl. generalize (X.eq_bool_ok y x); case (X.eq_bool y x); [intro y_eq_x; subst y | intro y_diff_x]; trivial. rewrite F in F'; discriminate. rewrite domain_of_subst_map_subst; trivial. Qed.
imports: Coq(Arith Wf_nat Wellfounded List Multiset Relations) CoLoR(closure decidable_set ordered_set more_list list_permut list_set list_sort dickson term_spec term)