proposition: Lemma indom_empty_eq : forall A B x, x \indom (\{}:map A B) = False.
proof: Proof. Proof using. intros. rewrite dom_empty. rewrite in_empty_eq. auto. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)