The Coq mailing list

[roconnor AT theorem.ca]

On Tue, 5 Dec 2006, Adam Chlipala wrote:

> My intuition is that this is impossible.  Since you aren't allowed to 
> eliminate values of types in Prop to construct values of types in Set,

Sometimes you can.  See 
<http://cocorico.cs.ru.nl/coqwiki/ExistsFromPropToSet>

for

Variable P : nat -> Prop.
Hypothesis P_dec : forall x, {P x} + {~ P x}.

Theorem prop_to_set : (exists x, P x) -> {x : nat | P x}.

And this can be used to solve the originial problem, assuming that P_dec 
can be satisfied.

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''