proposition: Lemma domain_update_id x s xs : domain xs (update x (Var x) s) [=] domain (remove x xs) s.
proof: Proof. intro y. rewrite !In_domain. set_iff. unfold Def.update. eq_dec y x. subst. tauto. fo. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)