proposition: Lemma finite_empty : finite (\{} : set A).
proof: Proof. Proof using. intros. apply finite_of_ex_list_covers. set_unf. exists (@nil A). introv M. inverts M. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibList LibOperation LibMonoid LibInt LibNat LibEpsilon LibRelation LibMin)