proposition: Lemma finite_empty : forall A B, finite (\{} : map A B).
proof: Proof. Proof using. intros. unfold finite. rewrite dom_empty. apply finite_empty. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)