proposition: Lemma vars_singles : forall x v us, vars_list (map (sub (single x v)) us) [=] if mem x (vars_list us) then union (vars v) (remove x (vars_list us)) else vars_list us.
proof: Proof. induction us; simpl; intros. refl. mem. trans (union (if mem x (vars a) then union (vars v) (remove x (vars a)) else vars a) (if mem x (vars_list us) then union (vars v) (remove x (vars_list us)) else vars_list us)). apply union_m. apply vars_single. exact IHus. case_eq (mem x (vars a)); case_eq (mem x (vars_list us)); intros; bool. trans (union (vars v) (union (remove x (vars a)) (remove x (vars_list us)))). apply union_idem_3. apply union_m. refl. sym. apply remove_union. trans (union (vars v) (union (remove x (vars a)) (vars_list us))). apply union_assoc. apply union_m. refl. trans (union (remove x (vars a)) (remove x (vars_list us))). apply union_m. refl. sym. apply remove_equal. apply mem_4. hyp. sym. apply remove_union. trans (union (vars v) (union (vars a) (remove x (vars_list us)))). apply union_sym_2. apply union_m. refl. trans (union (remove x (vars a)) (remove x (vars_list us))). apply union_m. sym. apply remove_equal. apply mem_4. hyp. refl. sym. apply remove_union. refl. Qed.
imports: CoLoR(LogicUtil ASubstitution FSetUtil NatUtil BoolUtil EqUtil ATrs ListUtil VecUtil) Coq(OrderedTypeEx)