---

Step * of Lemma lookup-list-map-eqKey_wf

∀[Key:Type]. ∀[keyDeq:EqDecider(Key)].  (lookup-list-map-eqKey(keyDeq) ∈ EqDecider(Key))
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[Key:Type].  \mforall{}[keyDeq:EqDecider(Key)].    (lookup-list-map-eqKey(keyDeq)  \mmember{}  EqDecider(Key))


By

---

Latex:
ProveWfLemma

---

Home Index