The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

Is it true that all goals in a proof subtree that has a Prop root are uninformative?  For example, consider the following:

Variable Foo : Set.

Inductive Bar : Prop :=
| bar : Foo -> Bar.

Goal (exists (f:Foo), True) -> Bar.
intro H.
constructor. (*switches goal from Prop to Set*)
Fail destruct H.
Abort.

Coq is preventing case analysis of the ex hypothesis H because the goal Foo is in Set (of course, merely exchanging the constructor and destruct H lines would make things work - but that is besides the point here).  However, its parent goal, Bar, is in Prop.  Is this simply Coq being overly conservative with case analysis?  If not, is there a way for a non-Prop subgoal in a subtree rooted in a Prop goal to impact extraction?

-- Jonathan