Skip to content

Add soundness lemma for envs_clear_intuitionistic

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.

Merge request reports