---

Step * of Lemma lookup-list-map-find_wf

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

---

Latex:

---

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


By

---

Latex:
ProveWfLemma

---

Home Index