The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

gallais @ ensl.org wrote:
> Hi Adam,
>
> My first guess would have been to follow closely
> the function's definition with something like:
>
> [pose (res := f n) ; destruct res ; simpl]
>
> and it turns out to work:
>
> [...]
> Is your approach more robust if we end up changing
> rK's definition or is it more or less equivalent (I'm guessing
> that pattern&  pose do the same job here).
>    

Well now, that's embarrassing!  Now I see this meager proof script also 
gets the job done:
    inversion 1; reflexivity.
Apparently [inversion] is smarter than I thought!