This makes it consistent with similar lemmas, e.g., auth_auth_valid.
The direction is now ✓{n} (● a) ↔ ✓{n} a.
@iris-users This is a breaking change, but I don't expect many developments to be affected by it.
This makes it consistent with similar lemmas, e.g., auth_auth_valid.
The direction is now ✓{n} (● a) ↔ ✓{n} a.
@iris-users This is a breaking change, but I don't expect many developments to be affected by it.