---

Step * of Lemma DVp_Struct_wf

∀[lbls:Atom List]. ∀[struct:{a:Atom| (a ∈ lbls)}  ⟶ C_DVALUEp()].  (DVp_Struct(lbls;struct) ∈ C_DVALUEp())
BY
{ DepprodCoDatatypeConstructorWf `C_DVALUEp_size` }

---

Latex:

---

Latex:
\mforall{}[lbls:Atom  List].  \mforall{}[struct:\{a:Atom|  (a  \mmember{}  lbls)\}    {}\mrightarrow{}  C\_DVALUEp()].
    (DVp\_Struct(lbls;struct)  \mmember{}  C\_DVALUEp())


By

---

Latex:
DepprodCoDatatypeConstructorWf  `C\_DVALUEp\_size`

---

Home Index