proposition: Lemma total_acc_inst_elim_var : forall c sigma v, var_in_term v (apply_subst sigma (Var v)) = false -> (forall x x_val, find X.eq_bool x sigma = Some x_val -> var_in_term v x_val = false) -> forall t, var_in_term v (apply_subst (acc_inst c sigma) t) = false.
proof: Proof. intro c; induction c as [ | v c]; intros sigma x x_elim_x sigma_elim_x t; simpl. pattern t; apply term_rec3; clear t. case_eq (find X.eq_bool x sigma); [intro x_val | idtac]; intro x_sigma; simpl in x_elim_x; rewrite x_sigma in x_elim_x. intros v; simpl; case_eq (find X.eq_bool v sigma); [intro v_val | idtac]; intro v_sigma. apply (sigma_elim_x v v_val v_sigma). simpl; generalize (X.eq_bool_ok v x); case (X.eq_bool v x); [intro v_eq_x | intros _; reflexivity]. subst v; rewrite x_sigma in v_sigma; discriminate. apply False_rect; revert x_elim_x; simpl. generalize (X.eq_bool_ok x x); case (X.eq_bool x x); [intros _; discriminate | intros x_diff_x _; apply x_diff_x; reflexivity]. intros f l; simpl; induction l as [ | t l]; intro IH. trivial. simpl. generalize (apply_subst sigma t) (IH t (or_introl _ (eq_refl _))). intros [w | g k] H; rewrite var_in_term_list_equation. simpl in H; revert H; generalize (X.eq_bool_ok w x); case (X.eq_bool w x); [intros _ Abs; discriminate | intro w_diff_x]. generalize (X.eq_bool_ok x w); case (X.eq_bool x w); [intros x_eq_w _ | intros _ _]. absurd (w=x); subst; trivial. simpl; apply IHl. intros; apply IH; right; trivial. simpl in H; rewrite H; simpl; apply IHl; intros; apply IH; right; trivial. apply IHc. simpl. assert (F := find_map_subst x v (apply_subst sigma (Var v)) sigma). case_eq (find X.eq_bool x sigma); [intro x_val | idtac]; intro x_sigma; simpl in x_elim_x; rewrite x_sigma in x_elim_x; rewrite x_sigma in F; unfold DecVar.A in *; simpl in F; rewrite F; clear F. apply no_var_in_term_inv. case_eq (find X.eq_bool v sigma); [intro v_val | idtac]; intro v_sigma. apply (sigma_elim_x v v_val v_sigma). simpl; generalize (X.eq_bool_ok v x); case (X.eq_bool v x); [intro v_eq_x | intros _; reflexivity]. subst v; rewrite x_sigma in v_sigma; discriminate. trivial. trivial. case_eq (find X.eq_bool x sigma); [intro x_val | idtac]; intro x_sigma; simpl in x_elim_x; rewrite x_sigma in x_elim_x. intros y y_val' F. assert (F' := find_map_subst y v (apply_subst sigma (Var v)) sigma). case_eq (find X.eq_bool y sigma); [intro y_val | idtac]; intro y_sigma; rewrite y_sigma in F'; simpl in F'; rewrite F in F'. injection F'; clear F'; intro F'; subst y_val'; clear F. apply no_var_in_term_inv. assert (H := sigma_elim_x v). case_eq (find X.eq_bool v sigma); [intro v_val | idtac]; intro v_sigma. apply H; trivial. simpl; generalize (X.eq_bool_ok v x); case (X.eq_bool v x); [intro v_eq_x | intros _; reflexivity]. subst v; rewrite x_sigma in v_sigma; discriminate. apply (sigma_elim_x y); trivial. discriminate. revert x_elim_x; simpl; generalize (X.eq_bool_ok x x); case (X.eq_bool x x); [intros _; intros; discriminate | intros x_diff_x; apply False_rect; apply x_diff_x; reflexivity]. 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)