Skip to content

prove later commuting around equality one way

Ralf Jung requested to merge ralf/later-equiv into master

I tried also proving the other direction, which feels like it should hold in the model, but I could not find a proof. But anyway this is the direction I wanted.

I felt like we already should have a proof of this somewhere but could not find one.

Merge request reports