I have a statement that two lambdas are the same:
G : (fun s' : S => x = s') = (fun s' : S => y = s')
And I want to use this to prove x=y. My thinking is simple, replace that statement with (fun s' : S => x = s') y, use G to replace one lambda with the other, reduce to y=y, profit. My problem is in the first step, I can find no way of setting up a statement containing the application of one lambda that Coq doesn't immediately reduce to x=y. I want the unapplied lambda to 'stick around' for a moment so I get a chance to apply G.
This seems like it should be easy an just can't figure it out.
Indeed, replace (x=y) with (fun s' : S => x = s') y does not give anything useful since the conclusion is simplified. But this is not the case of change (x=y) with (fun s' : S => x = s') y that you can use here to do what you want.
However, the simplest approach is probably pattern y which directly transforms the conclusion into the appropriate form.