Require Canonical Transformations To Be Unique Under Subsumption

[Checkmate50]

Canonical transformations are assumed to be unique -- there is exactly one canonical map between two coordinate systems. While this is not in fact always true (read: homogeneous coordinates), it is both best practice and most sensical to treat them as such. The only reason we currently do not do this is to allow the norm to homogeneous coordinates hack, something that was found to be done incorrectly from a type perspective.

Practically this means that invocations of in should fail if there are multiple ways to reach label B from label A in a single step (including subsumption). Note that this does not require checking if multiple paths exist over the course of several steps, as we assume that the programmer has checked that each of these paths are equivalent (see https://github.com/cucapra/linguine/wiki/Tutorial:-Casting-and-In-Expressions for details).

[Checkmate50]

We should add tests to check this