---

Step * of Lemma update-assignment_wf

∀[Dom:Type]. ∀[a:FOAssignment(Dom)]. ∀[x:ℤ]. ∀[v:Dom].  (a[x := v] ∈ FOAssignment(Dom))
BY
{ (ProveWfLemma THEN Unfold `FOAssignment` 0 THEN Auto) }

---

Latex:


\mforall{}[Dom:Type].  \mforall{}[a:FOAssignment(Dom)].  \mforall{}[x:\mBbbZ{}].  \mforall{}[v:Dom].    (a[x  :=  v]  \mmember{}  FOAssignment(Dom))


By

(ProveWfLemma  THEN  Unfold  `FOAssignment`  0  THEN  Auto)

---

Home Index