proposition: Lemma indom_empty_inv : forall A B (x:A), x \indom (\{} : map A B) -> False.
proof: Proof. Proof using. introv M. rewrite indom_empty_eq in M. auto. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)