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