---

Step * of Lemma C_TYPE-of-LVALUE_wf

∀env:C_TYPE_env(). ∀lval:C_LVALUE().  (C_TYPE-of-LVALUE(env;lval) ∈ C_TYPE()?)
BY
{ (Unfold `C_TYPE_env` 0 THEN ProveWfLemma) }

---

Latex:

---

Latex:
\mforall{}env:C\_TYPE\_env().  \mforall{}lval:C\_LVALUE().    (C\_TYPE-of-LVALUE(env;lval)  \mmember{}  C\_TYPE()?)


By

---

Latex:
(Unfold  `C\_TYPE\_env`  0  THEN  ProveWfLemma)

---

Home Index