proposition: Lemma finite_single : forall (a : A), finite \{a}.
proof: Proof. Proof using. intros. apply finite_of_ex_list_covers. set_unf. exists (a::nil). introv M. hnf in M. subst*. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibList LibOperation LibMonoid LibInt LibNat LibEpsilon LibRelation LibMin)