- add an intermediate step to the proof of "transitive reduction entails freshness consistency"