prove later commuting around equality one way

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.