Skip to content

Fix direction of `auth_auth_validN`

Robbert Krebbers requested to merge robbert/auth_auth_validN into master

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.

Merge request reports