proposition: Lemma dom_update : forall A B i v (M:map A B), dom (M[i:=v]) = (dom M \u \{i}).
proof: Proof. Proof using. intros. rewrite update_impl_eq. simpl. unfold dom_impl, union_impl, binds_impl in *. apply in_extens. intros x. rew_set. iff R. case_if~. case_if~. destruct~ R. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)