---

Step * of Lemma C_type_of_field_wf

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

1
1. ctyp : C_TYPE()
2. ↑C_Struct?(ctyp)
3. a : Atom
4. ↑C_field_of(a;ctyp)
⊢ ↑isl(apply-alist(AtomDeq;C_Struct-fields(ctyp);a))

---

Latex:

---

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


By

---

Latex:
ProveWfLemma

---

Home Index