proposition: Lemma disjoint_single_of_not_indom : forall A B (M:map A B) x (v:B), ~ x \indom M -> disjoint (x\:=v) M.
proof: Proof. Proof using. introv N. unfold disjoint, disjoint_inst, disjoint_impl. unfold single_bind, single_bind_inst, single_bind_impl, dom_impl. rewrite set_disjoint_eq. intros x'. repeat rewrite in_set_st_eq. case_if; subst; auto_false. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)