Test for equality

[jamievicary]

It would be good to add a test for equality (up to alpha equivalence) into our syntax. That would allow us to write .catt files that test the normalization functionality, e.g. to test that a given term A normalizes correctly to a second term B.

[ericfinster]

You can now write "eqnf ..ctx... | tm1 | tm2" and catt will check that the terms are equal. (for the moment, no normalization is done, but I will add that later). See the demo file for an example.

[jamievicary]

This is great.