proposition: Lemma singleton_finite : forall (x:A), finite (LibContainer.single x).
proof: Proof. Proof using. intros. exists (x::nil). intros y. rewrite in_single_eq. intro_subst. constructor. Qed.
imports: TLC(LibTactics LibList) TLC(LibSet LibLogic LibEqual LibReflect)