# Best way to express that a type is inhabited in a way that allows getting the habitant

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?

You can try to move your assumption to `Type`:

``````  forall P,
let S := {n : nat | P n} in
{ s : S | True } -> (forall s : S, exists s' : S, proj1_sig s < proj1_sig s')
-> infinite S.
``````

but since the predicate used here is `True`, you could simply write:

``````  forall P,
let S := {n : nat | P n} in
forall s : S, (forall s : S, exists s' : S, proj1_sig s < proj1_sig s')
-> infinite S.
``````

and you will probably face the same problem with `exists s'` which could be put into `Type` as well:

``````  forall P,
let S := {n : nat | P n} in
forall s : S, (forall s : S, { s' : S | proj1_sig s < proj1_sig s'})
-> infinite S.
``````