---

Step * of Lemma lookup-list-map-empty-prop

∀[Key:Type]. ∀[deqKey:EqDecider(Key)]. ∀[key:Key].  (¬↑lookup-list-map-inDom(deqKey;key;lookup-list-map-empty()))
BY
{ (RepUR ``lookup-list-map-inDom lookup-list-map-empty`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Key:Type].  \mforall{}[deqKey:EqDecider(Key)].  \mforall{}[key:Key].
    (\mneg{}\muparrow{}lookup-list-map-inDom(deqKey;key;lookup-list-map-empty()))


By

---

Latex:
(RepUR  ``lookup-list-map-inDom  lookup-list-map-empty``  0  THEN  Auto)

---

Home Index