The one place for your designs
To enable design management, you'll need to meet the requirements. If you need help, reach out to our support team for assistance.
`is_closed_expr` is stronger than stability under `subst`
I think there is a discrepancy between the substitution and is_closed_expr for heap_lang
According to subst,
subst x v' (of_val v) = of_val v.
However, is_closed_expr (of_val v) = is_closed_val v (https://gitlab.mpi-sws.org/FP/iris-coq/blob/master/theories/heap_lang/metatheory.v#L22) which is not always true.
That means, IIUC, that there are expressions that are not closed, but which are idempotent under the substitution.