---

Step * of Lemma DVp_Struct-lbls_wf

∀[v:C_DVALUEp()]. DVp_Struct-lbls(v) ∈ Atom List supposing ↑DVp_Struct?(v)
BY
{ DepprodCoDatatypeSelectorWf }

---

Latex:


\mforall{}[v:C\_DVALUEp()].  DVp\_Struct-lbls(v)  \mmember{}  Atom  List  supposing  \muparrow{}DVp\_Struct?(v)


By

DepprodCoDatatypeSelectorWf

---

Home Index