Hi,

Here is a small example demonstrating the gist of my question:

```
Definition injective {A B : Type} (f : A -> B)
:= forall a a', f a = f a' -> a = a'.
Definition infinite (T : Type) := exists (f : nat -> T), injective f.
Goal
forall P,
let S := {n : nat | P n} in
(exists s : S, True) /\ (forall s : S, exists s' : S, proj1_sig s < proj1_sig s')
-> infinite S.
Proof.
intros P S H. destruct H as [init succ].
unshelve eexists (fix f (n : nat) := (_ : S)).
* Fail destruct init.
(* “Case analysis on sort Set is not allowed for inductive definition ex.” *)
```

As you can see, the proof is stuck trying to destruct `exists s : S, True`

to extract an `s : S`

, because the result of this whole pattern matching needs to be of type `S`

, to exhibit a function `f : nat -> S`

, and as far as I understand, Coq does not allow a pattern matching on a `Prop`

to yield a non-`Prop`

in order to be able to erase `Prop`

s during extraction.

I can work around that by replacing `(exists s : S, True) /\ ...`

with `prod S ...`

, but then for other parts of the proof I also need to replace the `exists s : S', ...`

. I suppose I could also define a `myexists`

the same way as `exists`

but not in `Prop`

, then my custom `forall`

so it accepts something not in `Prop`

, and … Uh.

Is there a simple way to express and prove this theorem?