---

Step * of Lemma C_field_of_wf

∀[a:Atom]. ∀[ctyp:{t:C_TYPE()| ↑C_Struct?(t)} ].  (C_field_of(a;ctyp) ∈ 𝔹)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[a:Atom].  \mforall{}[ctyp:\{t:C\_TYPE()|  \muparrow{}C\_Struct?(t)\}  ].    (C\_field\_of(a;ctyp)  \mmember{}  \mBbbB{})


By

---

Latex:
ProveWfLemma

---

Home Index