The proof that excluded middle follows if all subsets of a singleton set are finite.

finite_subsets_and_LEM.v

(* If all subsets of a singleton set are finite, then excluded middle holds.*)
Require Import List.

(* We present the subsets of X as characteristic maps S : X -> Prop.
   Thus to say that x : X is an element of S : Powerset X we write S x. *)
Definition Powerset X := X -> Prop.

(* Auxiliary relation "l lists the elements of S". *)
Definition lists {X} (l : list X) (S : Powerset X) :=
  forall x, S x <-> In x l.

(* A subset is finite if its elements are listed by some list. *)
Definition finite_subset {X} (S : Powerset X) :=
  exists l : list X, lists l S.

(* The subset listed by the empty list is the empty subset. *)
Lemma nil_empty {X} (S : Powerset X) :
  lists nil S -> forall x, ~ S x.
Proof.
  intros H x Sx.
  now apply (H x).
Qed.

(* Statement of excluded middle. *)
Definition LEM := (forall p, p \/ ~p).

(* If all subsets of the singleton are finite then excluded middle holds. *)
Theorem finite_lem:
  (forall S : unit -> Prop, finite_subset S) -> LEM.
Proof.
  (* suppose all subsets of unit are finite, and consider any proposition p *)
  intros H p.
  (* the subset (fun _ => p) is listed either by nil or (cons tt ...). *)
  destruct (H (fun _ => p)) as [[|[]] L].
  - (* if it is listed by the empty list, then ~p follows *)
    right.
    apply (nil_empty _ L tt).
  - (* if it is listed by (const tt ...) then p follows. *)
    left.
    apply (L tt).
    now left.
Qed.