---

Step * of Lemma record-update_wf

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

---

Latex:

---

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


By

---

Latex:
(Unfold  `record`  0  THEN  ProveWfLemma)

---

Home Index