---

Step * 1 of Lemma lookup-list-map-inDom-prop


1. Key : Type
2. Value : Type
3. deqKey : EqDecider(Key)
4. key : Key
⊢ ↑lookup-list-map-inDom(deqKey;key;[]) ⇐⇒ ↑isl(lookup-list-map-find(deqKey;key;[]))
BY
{ (RepUR ``lookup-list-map-inDom lookup-list-map-find apply-alist`` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  Key  :  Type
2.  Value  :  Type
3.  deqKey  :  EqDecider(Key)
4.  key  :  Key
\mvdash{}  \muparrow{}lookup-list-map-inDom(deqKey;key;[])  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}isl(lookup-list-map-find(deqKey;key;[]))


By

---

Latex:
(RepUR  ``lookup-list-map-inDom  lookup-list-map-find  apply-alist``  0  THEN  Auto)

---

Home Index