---

Step * of Lemma LV_Ground_wf

∀[loc:C_LOCATION()]. (LV_Ground(loc) ∈ C_LVALUE())
BY
{ DepprodCoDatatypeConstructorWf `C_LVALUE_size` }

---

Latex:


\mforall{}[loc:C\_LOCATION()].  (LV\_Ground(loc)  \mmember{}  C\_LVALUE())


By

DepprodCoDatatypeConstructorWf  `C\_LVALUE\_size`

---

Home Index