<p>I found a way to get it to work without any additional axioms using the &quot;not not&quot; technique from &quot;Classical Mathematics for a Constructive World&quot; <a href="https://arxiv.org/pdf/1008.1213.pdf" rel="nofollow noreferrer">https://arxiv.org/pdf/1008.1213.pdf</a></p>
<p>(I haven't tried to clean up the proofs at all, just to get it to type check.  Sorry for weird phrasing in proofs.)</p>
<pre><code>Require Import Coq.Sets.Ensembles.

(* Classical reasoning without extra axioms. *)
Definition stable P := ~~P -&gt; P.

Theorem stable_False : stable False.
  unfold stable; intros nnF.
  apply nnF; intros f.
  apply f.
Qed.

Definition orW P Q := ~(~P /\ ~Q).

Definition exW {A} (P : A -&gt; Prop) := ~(forall a, ~P a).

Theorem exW_strengthen {A} P Q (stQ : stable Q) (exQ : (exists a, P a) -&gt; Q) (exWP : exW (fun (a : A) =&gt; P a)) : Q.
  apply stQ; hnf; intros.
  apply exWP; intros; hnf; intros.
  apply H; apply exQ; apply (ex_intro _ _ H0).
Qed.


(* Ensembles *)
Definition emptyOnly A := Singleton _ (Empty_set A).

Theorem notEmpty_In A (s : Ensemble A) (ne : ~ Same_set _ s (Empty_set _)) : exW (fun a =&gt; In _ s a).
  hnf; intros; apply ne; clear ne.
  apply conj; hnf; intros; [ | destruct H0 ].
  apply (False_ind _ (H _ H0)).
Qed.

Theorem enumerateSingletonPowerset A s (inc : Included _ s (emptyOnly A)):
  orW (Same_set _ s (Empty_set _)) (Same_set _ s (emptyOnly A)).
  hnf; intros; destruct H.
  apply notEmpty_In in H.
  revert H; apply exW_strengthen; intros; [ apply stable_False | ]; destruct H.
  apply H0; clear H0; apply conj; hnf; intros; [ apply (inc _ H0) | ].
  destruct H0.
  destruct (inc _ H).
  apply H.
Qed.
</code></pre>
<p>So, by rephrasing the theorem to use weak or, it is now possible to prove it directly, and without appealing to the structure of A, that membership is decidable, or classical logic.</p>
How to enumerate set in Coq Ensemble
<p>How do you prove <code>enumerateSingletonPowerset</code>?</p>
<pre><code>Require Import Coq.Sets.Ensembles.

Definition emptyOnly A := Singleton _ (Empty_set A).

Theorem enumerateSingletonPowerset A s (inc : Included _ s (emptyOnly A)):
  Same_set _ s (Empty_set _) \/ Same_set _ s (emptyOnly A).
</code></pre>
<p>I'm using <code>Same_set</code> to avoid extensionality.  (Either way is fine.)</p>
<p>Conceptually, it seems simple to just say I have
<code>{{}}</code>
so the powerset is
<code>{{}, {{}}}</code>
and that's it.  But, it's not clear how to say anything like that with these primitives on their own.</p>
<p>I'd be tempted to try destructing on if empty set was in the set s.  But, since Emsemble is propositional, checking set membership is not generally decidable.  A first thought is</p>
<pre><code>Axiom In_dec : forall A a e, In A e a \/ ~In A e a.

Theorem ExcludedMiddle P : P \/ ~P.
  apply (In_dec _ tt (fun _ =&gt; P)).
Qed.
</code></pre>
<p>But, that is too powerful and immediately puts me into classical logic.  The finite case is easy, but I plan on dealing with larger sets (e.g. Reals), so In and Included would not generally be computable.  Are there axioms I could add that could allow In and Included to pretend to be decidable without making everything else decidable too?</p>
<p>Edit: Changed from pair to singleton since quantity isn't important.</p>