proposition: Lemma update_eq_union_single : forall A B (M:map A B) k x, M[k:=x] = M \u (k \:= x).
proof: Proof. Proof using. auto. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)