The Coq mailing list

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

On 07/09/2012 09:03 AM, Denis Cousineau wrote:
> I've found that the tactic subst  only works with equations in contexts that 
> concern variables that were quantified in the goal, and not global parameters.
>    

I imagine this issue hasn't bothered others because use of global 
parameters is strongly discouraged; it's really against the spirit of 
constructive logic!

But, you can easily get [subst] to behave as you wish for parameter [x] 
by running:
    generalize dependent x; intros; subst.