Equality elimination appears to be broken

[esotechnica]

See details at the following link:

https://math.stackexchange.com/questions/2601281/whats-wrong-with-this-proof-of-symmetry-of-equality/2602046#2602046

[rzach]

Confirmed also on Kevin's original. It's not a stable bug; works most of the time.

[frabjous]

Richard,

I fixed this bug and committed the change to the repo. But you'll need to implement the change to where you have the demo on the website.

-Kevin

On Fri, Jan 12, 2018 at 7:22 AM, esotechnica notifications@github.com wrote:

See details at the following link:

https://math.stackexchange.com/questions/2601281/whats- wrong-with-this-proof-of-symmetry-of-equality/2602046#2602046 http://url

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/OpenLogicProject/fitch-checker/issues/6, or mute the thread https://github.com/notifications/unsubscribe-auth/AASrHCKNBTGdEjFnTZpxZw2-kB8Y20Rpks5tJ06OgaJpZM4RcOFe .

[frabjous]

Incidentally, the problem was not with =E, but with sameWff as applied to identity statements. Not worth trying to explain here.

[rzach]

Thanks @frabjous Fixed in 6b21373f0d08853715b18726122b54695a0179df

[rzach]

(The fix is live on the website too)