---

Step * of Lemma LV_Index_wf

∀[lval:C_LVALUE()]. ∀[idx:ℤ].  (LV_Index(lval;idx) ∈ C_LVALUE())
BY
{ DepprodCoDatatypeConstructorWf `C_LVALUE_size` }

---

Latex:

---

Latex:
\mforall{}[lval:C\_LVALUE()].  \mforall{}[idx:\mBbbZ{}].    (LV\_Index(lval;idx)  \mmember{}  C\_LVALUE())


By

---

Latex:
DepprodCoDatatypeConstructorWf  `C\_LVALUE\_size`

---

Home Index