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.
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.