The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 03/08/2014 17:47, Jonathan wrote:
> What is so different about a nat vs. a sig that allows the analysis of
> the ex H in the sig goal but not the nat goal?

This is due to a weak form of universe polymorphism of the old
inductives. In your case, the sig that usually lives in Type collapse
into Prop because all of its arguments are from Prop.

Variable A : Prop.
Variable P : A -> Prop.

Check {x : A | P x}.

{x : A | P x} : Prop

I do not know if this is documented somewhere, but this phenomenon
occurs with all inductives which do not provide a relevant content
whenever their parameters are instantiated with Prop-living types. This
is the case with one-constructor inductives, like sig, prod & eq.
PMP

Attachment: signature.asc
Description: OpenPGP digital signature