---

Step * of Lemma lookup-list-map-update_wf

∀[Key,Value:Type]. ∀[deqKey:EqDecider(Key)]. ∀[key:Key]. ∀[val:Value]. ∀[m:lookup-list-map-type(Key;Value)].
  (lookup-list-map-update(deqKey;key;val;m) ∈ lookup-list-map-type(Key;Value))
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[Key,Value:Type].  \mforall{}[deqKey:EqDecider(Key)].  \mforall{}[key:Key].  \mforall{}[val:Value].
\mforall{}[m:lookup-list-map-type(Key;Value)].
    (lookup-list-map-update(deqKey;key;val;m)  \mmember{}  lookup-list-map-type(Key;Value))


By

---

Latex:
ProveWfLemma

---

Home Index