proposition: Lemma eq_union_restrict_remove_one : forall A (x:A) B `{Inhab B} (M:map A B), x \indom M -> M = (M \- \{x}) \u (x \:= (M[x])).
proof: Proof. Proof using. intros. rewrite~ <- restrict_single. apply eq_union_restrict_remove. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)