---

Step * of Lemma record-select_wf

∀[T:Atom ⟶ 𝕌']. ∀[z:Atom]. ∀[r:record(x.T[x])].  (r.z ∈ T[z])
BY
{ (Unfold `record` 0 THEN ProveWfLemma) }

---

Latex:

---

Latex:
\mforall{}[T:Atom  {}\mrightarrow{}  \mBbbU{}'].  \mforall{}[z:Atom].  \mforall{}[r:record(x.T[x])].    (r.z  \mmember{}  T[z])


By

---

Latex:
(Unfold  `record`  0  THEN  ProveWfLemma)

---

Home Index