---

Step * of Lemma C_Struct-fields_wf

∀[v:C_TYPE()]. C_Struct-fields(v) ∈ (Atom × C_TYPE()) List supposing ↑C_Struct?(v)
BY
{ DepprodCoDatatypeSelectorWf }

---

Latex:

---

Latex:
\mforall{}[v:C\_TYPE()].  C\_Struct-fields(v)  \mmember{}  (Atom  \mtimes{}  C\_TYPE())  List  supposing  \muparrow{}C\_Struct?(v)


By

---

Latex:
DepprodCoDatatypeSelectorWf

---

Home Index