Forked from
Iris / Iris
Source project has a limited visibility.
-
Jacques-Henri Jourdan authored
Lifting lemmas : make the initial state appear under an existential under the view shift. This is still sound, but slightly more expressive.
Jacques-Henri Jourdan authoredLifting lemmas : make the initial state appear under an existential under the view shift. This is still sound, but slightly more expressive.