`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.