Calc implication

[jaybosamiya]

This PR performs two changes:

1. Adds support for adding non-single-token relations to calc
2. Adds support for implication operators to calc to behave as relations (==> and <==>)

(1) is needed to support (2). In particular, the older version of calc assumed that each relation was a single token (or at least denoted via a single tt); unfortunately, operators like ==> and <==> are composed of multiple tokens. Thus, to support them, we need to carefully thread through repetitions of tts across the whole of the calc macro. This is what (1) does.

(2) then simply adds the minor additions. In fact, now that (1) is done, adding new relations should be as easy as this second one.

From a user-facing perspective, (1) should have no change at all, and (2) should start allowing calc to be used in more places.

To review this PR, it is likely easiest to read the commits for (1) and (2) separately.

Also, reminder to self: don't squash-and-commit (instead just rebase both commits); keeping these two commits separate will make it easier to understand how to add new operators to calc.

[jaybosamiya]

Oh, and adding some context around confirm_middle_relations and why it was needed (mostly a note to self in case I ever face similar issue around macros): without it, naively wrapping things with the $(..)* for each of the expressions almost works, except for the point at which the checks are done to give nicer messages on consistency of intermediate relations. At that point, there is trouble around differing repetition levels (in particular, $reln is at level 1 and $middlereln is at level 2). Differing repetition levels are supported only when they are all either a single level n or 0 (in particular, (0, 1) that existed before is fine, but (1, 2) that happened by naively wrapping with * is not fine). Thus, we need to get creative with the checking, by pushing them into not being forced into a level comparison at all. That trick is to introduce the new path confirm_middle_relations which flattens them out separately, and then internally proceeds in a line, thereby not needing separate levels.

None of the above explanation is essential to understanding the implementation, but serves only as an explanation to understand why it needed to change. Thus it is a comment here, rather than a comment in the code.

[utaal]

Thank you for the additional context and explanation. Looks good to me.