proposition: Lemma fvcodom_update_id x s xs : fvcodom xs (update x (Var x) s) [=] fvcodom (remove x xs) s.
proof: Proof. unfold Def.fvcodom. rewrite domain_update_id. set (d := domain (remove x xs) s). intro y. rewrite !In_fvcod. assert (h : ~In x d). unfold d. rewrite In_domain. set_iff. tauto. unfold Def.update; split; intros [a [h1 h2]]; ex a; eq_dec a x; subst; fo. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)