Skip to content
GitLab

Add soundness lemma for envs_clear_intuitionistic

Merged Simon Friis Vindum requested to merge simonfv/iris:clear-intuit-sound into master

There is a soundness lemma for envs_clear_spatial but not one for envs_clear_intuitionistic. This MR adds one for envs_clear_intuitionistic.