https://github.com/leanprover-community/iris-lean/pull/688 I've posted a few times about it but I think my work here is done. I am now very very pleased with this PR. Fully swapped the theory underlying Iris with essentially zero changes for clients (or at least for the HeapLang client). Might be my favorite piece of code I've ever written, I feel like a proof ninja.