-
Robbert Krebbers authored
There is no need to include the `(∃ P', □ ▷ (P
↔ P') ...` since we get closure under `▷ □↔ ` from regular invariants.707b6601
There is no need to include the `(∃ P', □ ▷ (P↔ P') ...` since we get closure under `▷ □↔ ` from regular invariants.