Optimize generated code when source and destination are the same

[ReedOei]

Note that we always have x --[ v ]-> x leaves x unchanged. Therefore, we should only do the necessary precondition checks in such cases (especially useful for only when).

Related: when we check a condition like only when x = y, we generate:

x --[ y ]-> x
y --[ x ]-> y

This is correct, but it is inefficient if x and y are not fungible; in this case, we generate:

require(x == y, ...);
require(y == x, ...);

which is redundant.