This closes issue #55 (closed).
Note that both arguments of TCEq are outputs, which makes TCEq symmetric. We could make one the input argument and the other the output argument, but this requires some change to Iris without obvious benefits.
/cc @msammler @janno
This will create a new commit in order to revert the existing changes.