Commit 77f2e6be authored by Amin Timany's avatar Amin Timany

Remove empty_env_subst as it's moved to typing now

parent 7f179e11
......@@ -201,11 +201,6 @@ Section Soundness.
{iI : heapIG Σ} {iS : cfgSG Σ}
{N : namespace}.
Lemma empty_env_subst e : e.[env_subst []] = e.
replace (env_subst []) with (@ids expr _) by reflexivity.
asimpl; trivial.
Qed.
Definition free_type_context : varC -n> bivalC -n> iPropG lang Σ :=
{| cofe_mor_car := λ x, {| cofe_mor_car := λ y, (True)%I |} |}.
......
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