---

Step * of Lemma LV_Scomp_wf

∀[lval:C_LVALUE()]. ∀[comp:Atom].  (LV_Scomp(lval;comp) ∈ C_LVALUE())
BY
{ DepprodCoDatatypeConstructorWf `C_LVALUE_size` }

---

Latex:


\mforall{}[lval:C\_LVALUE()].  \mforall{}[comp:Atom].    (LV\_Scomp(lval;comp)  \mmember{}  C\_LVALUE())


By

DepprodCoDatatypeConstructorWf  `C\_LVALUE\_size`

---

Home Index