proposition: Lemma dom_single : forall A B (k:A) (x:B), dom (k\:=x) = \{k}.
proof: Proof. Proof using. intros. simpl. unfold binds_impl, single_bind_impl, dom_impl. apply set_ext. intros y. rewrite in_set_st_eq. iff R; case_if~. rewrite in_single_eq. auto. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)