I'm trialling a proof verifying tool (found here), and have tried to prove the symmetry of equality in FOL, as shown by the attached screen shot
As you can see, it comes up with an error regarding the last line. What is wrong with this? Am I missing something simple? Or is this tool broken?
Looks as if the tool is broken, in the sense of not implementing Leibniz's Law properly, as the move from (3) and (4) to (5) is an unexceptional example of the application of LL.