proposition: Lemma vars_single : forall x v u, vars (sub (single x v) u) [=] if mem x (vars u) then union (vars v) (remove x (vars u)) else vars u.
proof: Proof. intros x v. apply term_ind with (Q := fun n (ts : terms n) => vars_vec (Vmap (sub (single x v)) ts) [=] if mem x (vars_vec ts) then union (vars v) (remove x (vars_vec ts)) else vars_vec ts). intro. simpl. unfold single. case_beq_nat x x0. autorewrite with mem Equal. refl. simpl. mem. rewrite (beq_com beq_nat_ok), H. refl. intros. rewrite sub_fun. case_eq (mem x (vars (Fun f v0))); rewrite !vars_fun; intro; rewrite H0 in H; exact H. refl. intros u n us. simpl. mem. intros. rewrite H, H0. case_eq (mem x (vars u)); intro H1; simpl. revert H1. case_eq (mem x (vars_vec us)); intro H2. trans (union (union (vars v) (remove x (vars u))) (union (vars v) (remove x (vars_vec us)))). refl. trans (union (vars v) (union (remove x (vars u)) (remove x (vars_vec us)))). apply union_idem_3. apply union_m. refl. sym. apply remove_union. trans (union (union (vars v) (remove x (vars u))) (vars_vec us)). apply union_m; refl. trans (union (vars v) (union (remove x (vars u)) (vars_vec us))). autorewrite with Equal. refl. apply union_m. refl. trans (union (remove x (vars u)) (remove x (vars_vec us))). apply union_m. refl. sym. apply remove_equal. apply mem_4. hyp. sym. apply remove_union. revert H1. case_eq (mem x (vars_vec us)); intros H2 H1. trans (union (vars u) (union (vars v) (remove x (vars_vec us)))). apply union_m; refl. trans (union (vars v) (union (vars u) (remove x (vars_vec us)))). apply union_sym_2. apply union_m. refl. trans (union (remove x (vars u)) (remove x (vars_vec us))). apply union_m. sym. apply remove_equal. apply mem_4. hyp. refl. sym. apply remove_union. apply union_m; refl. Qed.
imports: CoLoR(LogicUtil ASubstitution FSetUtil NatUtil BoolUtil EqUtil ATrs ListUtil VecUtil) Coq(OrderedTypeEx)