The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

CHA Reeseo wrote:
> QUESTION 1: Is there really no way to retrieve detailed information from
> the proofs of inductive predicates (whose final type is Prop) when the
> current goal has sort Set?
>    

There should not be a way.  If such a way were found, I would call it a 
bug.  The meaning of [Prop] is more or less "values that cannot be used 
to influence the behavior of extracted programs."  If you don't want 
that behavior, then you should code using [Set] versions of connectives 
that the Coq standard library puts in [Prop].  You would only be losing 
[Prop]'s impredicativity; everything else can be duplicated in [Set].

You also have the option of using one of the axioms of choice found in 
the Coq standard library.

>      1 subgoal
>
>        P : nat ->  Prop
>        x : nat
>        H : P x
>        ============================
>         P ?7
>
> QUESTION 2: Why 'eexact H' fails here?
>
>      foo<  eexact H.
>      Toplevel input, characters 0-8:
>      >  eexact H.
>      >  ^^^^^^^^
>      Error: Impossible to unify "?7" with "x".
>    

The unification variable [?7] was introduced before [x] was introduced.  
In other words, [?7] must be valid in a typing context that has no [x], 
so the instantiation may not mention [x].  If you try to do the proof by 
hand, in a very pedantic way, I think you will see why the step you are 
attempting is invalid, for simple syntactic reasons.