proposition: Lemma finite_single : forall A B (k : A) (x : B), finite (k\:=x).
proof: Proof. Proof using. intros. unfold finite. rewrite dom_single. apply finite_single. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)