The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

I thought that just the kind of goal (Prop vs, non-Prop), along with the 
particulars of a specific Prop (single constructor/no info vs 
otherwise), determine whether or not that Prop can be analyzed in a 
context.  But then I stumbled on this (works in the trunk):

Goal forall (A : Prop) (P : A -> Prop),
    (exists x, P x) -> {x : A | P x }.
intros A P H.
destruct H. eexists. exact H.
Qed.


Goal forall (A : Prop) (P : A -> Prop),
     (exists x, P x) -> nat.
intros A P H.
Fail destruct H.
Abort.

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?

More importantly, why prevent the destruct in the nat goal if it is 
allowed in the sig goal?

-- Jonathan