proposition: Lemma dom_eq_set_of_binds : forall A B (M:map A B), dom M = \set{ k | exists v, binds M k v }.
proof: Proof. Proof using. intros. simpl. unfold dom_impl, binds_impl. applys set_st_eq. intros k. iff R. destruct (M k). eauto. false. destruct R. congruence. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)