This makes it consistent with the Iris 1 appendix:
I think it also makes the spec strictly stronger because you learn the lock was unlocked before the linearization point.