---

Step * of Lemma DVp_Struct-struct_wf

∀[v:C_DVALUEp()]. DVp_Struct-struct(v) ∈ {a:Atom| (a ∈ DVp_Struct-lbls(v))}  ─→ C_DVALUEp() supposing ↑DVp_Struct?(v)
BY
{ DepprodCoDatatypeSelectorWf }

---

Latex:


\mforall{}[v:C\_DVALUEp()].  DVp\_Struct-struct(v)  \mmember{}  \{a:Atom|  (a  \mmember{}  DVp\_Struct-lbls(v))\}    {}\mrightarrow{}  C\_DVALUEp()  supposin\000Cg  \muparrow{}DVp\_Struct?(v)


By

DepprodCoDatatypeSelectorWf

---

Home Index