In first order logic, given F℩xFx, are you able to use alphabetical variation?

Question

I am deriving the statement: ∴ ℩xFx=℩yFy

This is what I have so far

I am not sure how to proceed from here. I noticed I have F℩xFx and ~F℩yFy

Would I be able to use alphabetical variation to change the x into a y or vice versa to prove the derivation?

Every time I try to use alphabetical variance, it tells me the parser "cannot map G℩xFx" — I am unsure of what this means.

Thanks in advance!