proposition: Lemma dom_empty_inv : forall A B (M : map A B), dom M = \{} -> M = \{}.
proof: Proof. Proof using. introv H. simpls. unfold dom_impl, empty_impl in *. extens ;=> k. absurds ;=> G. lets R: @is_empty_inv k H. typeclass. false R. rewrite~ in_set_st_eq. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)