The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 07/23/2012 11:43 AM, Wolfram Kahl wrote:
> ``gallais'' wrote:
>
>   >  Lemma IsSome_extract : forall A (x : option A), IsSome x ->  { r | x = 
> Some r }.
>   >  Proof.
>   >  intros A x Hx ; destruct x.
>   >   exists a ; reflexivity.
>   >   apply False_rect.
>   >    inversion Hx.
>   >  Qed.
>
> (That additional equation is indeed essential, and I also had produced
>   it for the other definition in the meantime.)
> I found it surprising that ``inversion Hx'' works here,
> while in my attempt (without the False_rect of gallais),
> it produces a sort error.
>    

The key is that he first applied [False_rect] to move into [Prop].  
(This is exactly the Curry-Howard analogue of my advice.)

P.S.: I really advise _not_ using tactics to build dependently typed 
definitions with computational content.