proposition: Lemma restrict_single : forall A (x:A) `{Inhab B} (M:map A B), x \indom M -> M \| \{x} = (x \:= (M[x])).
proof: Proof. Proof using. introv N. applys fun_ext_1. intros k. simpls. unfolds dom_impl, restrict_impl, single_bind_impl, read_impl. rew_set in *. do 2 case_if~. subst. destruct (M x); auto_false. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)