---

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

∀[Key,Value:Type]. ∀[deqKey:EqDecider(Key)]. ∀[key:Key]. ∀[m:lookup-list-map-type(Key;Value)].
  (↑lookup-list-map-inDom(deqKey;key;m) ⇐⇒ ↑isl(lookup-list-map-find(deqKey;key;m)))
BY
{ ((UnivCD THENA Auto) THEN Unfold `lookup-list-map-type` (-1) THEN ListInd (-1) THEN Try (CpltAuto)) }

1
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;[]))

2
1. Key : Type
2. Value : Type
3. deqKey : EqDecider(Key)
4. key : Key
5. u : Key × Value@i
6. v : (Key × Value) List@i
7. ↑lookup-list-map-inDom(deqKey;key;v) ⇐⇒ ↑isl(lookup-list-map-find(deqKey;key;v))@i
⊢ ↑lookup-list-map-inDom(deqKey;key;[u / v]) ⇐⇒ ↑isl(lookup-list-map-find(deqKey;key;[u / v]))

---

Latex:

---

Latex:
\mforall{}[Key,Value:Type].  \mforall{}[deqKey:EqDecider(Key)].  \mforall{}[key:Key].  \mforall{}[m:lookup-list-map-type(Key;Value)].
    (\muparrow{}lookup-list-map-inDom(deqKey;key;m)  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}isl(lookup-list-map-find(deqKey;key;m)))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  Unfold  `lookup-list-map-type`  (-1)  THEN  ListInd  (-1)  THEN  Try  (CpltAuto))

---

Home Index