Commit d4423268 authored by Simon Friis Vindum's avatar Simon Friis Vindum
Browse files

Add changelog entry for big_sepM implication lemmas

parent bd1e14de
Pipeline #51354 passed with stage
in 8 minutes and 32 seconds
......@@ -68,6 +68,8 @@ Coq 8.11 is no longer supported in this version of Iris.
by combining the embeddings of `PROP1` into `PROP2` and `PROP2` into `PROP3`.
This construct is *not* declared as an instance to avoid TC search divergence.
(by Hai Dang, BedRock Systems)
* Add the lemmas `big_sepM_impl_strong` and `big_sepM_impl_dom_subseteq` that
generalize the existing `big_sepM_impl` lemma.
**Changes in `proofmode`:**
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment