proposition: Lemma fvcod_single y v : forall xs, fvcod xs (single y v) [=] if mem y xs then union (fv v) (remove y xs) else xs.
proof: Proof. apply set_induction_bis. intros s s' ss'. rewrite ss'. intro h. rewrite h. destruct (mem y s'); rewrite ss'; refl. rewrite fvcod_empty, empty_b. refl. intros x u n IH. rewrite fvcod_add, IH. 2: hyp. clear IH. unfold Def.fvcod_fun, Def.single, Def.update, eqb. eq_dec x y; simpl. subst y. rewrite add_b, eqb_refl. simpl. rewrite not_mem_iff in n. rewrite n. rewrite <- not_mem_iff in n. intro a. set_iff. split. intros [a1|a1]. auto. right. split. auto. intro e. subst. fo. intros [a1|[[a1|a1] a2]]; auto. subst. cong. rewrite <- eqb_false_iff in n0. rewrite add_b, n0. simpl. case_eq (mem y u); [rewrite <- mem_iff|rewrite <- not_mem_iff]; intro hy. intro a. set_iff. split. intros [a1|[a1|[a1 a2]]]; auto. right. split. auto. intro e. subst. rewrite eqb_false_iff in n0. cong. intros [a1|[[a1|a1] a2]]; auto. sym. apply add_union_singleton. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)