---

Step * of Lemma C_LVALUE_size_wf

∀[p:C_LVALUE()]. (C_LVALUE_size(p) ∈ ℕ)
BY
{ ProveCoSizeWf2 `C_LVALUEco_size` }

---

Latex:


\mforall{}[p:C\_LVALUE()].  (C\_LVALUE\_size(p)  \mmember{}  \mBbbN{})


By

ProveCoSizeWf2  `C\_LVALUEco\_size`

---

Home Index