proposition: Lemma dom_empty : forall A B, dom (\{} : map A B) = (\{} : set A).
proof: Proof. Proof using. intros. simpl. unfold dom_impl. simpl. unfold binds_impl, empty_impl. apply set_ext. intros x. rewrite in_set_st_eq. iff R. false. false. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)