proposition: Lemma eq_empty_of_not_indom : forall A B (IB:Inhab B) (M:map A B), (forall x, ~ x \indom M) -> M = \{}.
proof: Proof. Proof using. introv IB H. applys extensionality. { intros x. rewrite indom_empty_eq. iff*. } { intros x Dx. false* H. } Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)