Should we be using `=` instead of equiv `===` on the spine?

[NicMcPhee]

At the moment we're using equiv (===) on the spine for equivalence/equality steps. It was suggested at a recent demo/feedback session that Gries & Schneider use "regular" equality (=) to indicate that the spine should be read as "A=B and B=C and C=D…" instead of in the associative manner of equivalence.

I should check the book (don't have one here), and if that's true (and it seems reasonable) we should change the checker to use this syntax.