I'm in the middle of completing a proof, and need to show that b=a. I already have a=b. I think this should be trivial, however, I cannot find a way to do it inside the system.
Using the programs "Ana-Con" feature, it does indeed suggest that this is true within the system, but I can't find a way to do this without using this shortcut.
Anyone have any suggestions?