Evaluation-context language
We should have a typeclass for an evaluation-context based language, and an instance to convert these into a general Iris language, and some specialized lifting lemmas for such languages.
We should have a typeclass for an evaluation-context based language, and an instance to convert these into a general Iris language, and some specialized lifting lemmas for such languages.