proposition: Lemma elim_var_in_subst : forall sigma v v_val z, VSet.mem z (domain_of_subst sigma) -> var_in_term v v_val = false -> var_in_term v (apply_subst (map_subst (fun _ t => apply_subst ((v,v_val) :: nil) t) sigma) (Var z)) = false.
proof: Proof. intros sigma v v_val y y_in_dom v_in_v_val. simpl; rewrite var_in_domain_of_subst in y_in_dom. assert (F := find_map_subst y v v_val sigma). case_eq (find X.eq_bool y sigma); [intro y_val | idtac]; intro y_sigma; rewrite y_sigma in F; rewrite F. assert (var_in_term v (apply_subst ((v, v_val) :: nil) y_val) <> true). intro H1; rewrite var_in_term_is_sound in H1. destruct (var_in_subterm2 _ _ (in_impl_mem (@eq _) (fun a => eq_refl a) _ _ H1)) as [p H''']. assert (H4 := subterm_in_instantiated_term _ _ _ H'''). case_eq (subterm_at_pos y_val p); [intros [w | f l] | idtac]; intro Hsub; rewrite Hsub in H4. simpl in H4; revert H4; generalize (X.eq_bool_ok w v); case (X.eq_bool w v); [intro w_eq_v | intro w_diff_v]. intro H4; subst w v_val; assert (v_in_v_val' : var_in_term v (Var v) = true). simpl; generalize (X.eq_bool_ok v v); case (X.eq_bool v v); [intros _; trivial | intro v_diff_v; apply False_rect; apply v_diff_v; reflexivity]. rewrite v_in_v_val in v_in_v_val'; discriminate. intro H4; apply w_diff_v; injection H4; clear H4; intro H4; subst w; trivial. discriminate. destruct H4 as [w [q [q' [H4 [H5 [H6 H7]]]]]]. simpl in H7; revert H7; generalize (X.eq_bool_ok w v); case (X.eq_bool w v); [intro w_eq_v | intro w_diff_v]. intro H7; subst w; assert (x_in_v_val := var_in_subterm v _ _ H7 (or_introl _ (eq_refl _))). rewrite <- var_in_term_is_sound in x_in_v_val. rewrite v_in_v_val in x_in_v_val; discriminate. intro H7; destruct q'; [injection H7; clear H7; intro H7; subst w | discriminate]. apply w_diff_v; trivial. destruct (var_in_term v (apply_subst ((v, v_val) :: nil) y_val)); [absurd (true = true) | idtac]; trivial. rewrite y_sigma in y_in_dom; absurd (@None term = None); 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)