---

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


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]))
BY
{ (DProds
   THEN RepUR ``lookup-list-map-inDom lookup-list-map-find eqof`` 0
   THEN (BoolCase ⌜deqKey key u1⌝⋅ THEN Try (CpltAuto))
   THEN BoolCase ⌜deqKey u1 key⌝⋅
   THEN Try (CpltAuto)) }

1
1. Key : Type
2. Value : Type
3. deqKey : EqDecider(Key)
4. key : Key
5. u1 : Key@i
6. ¬(u1 = key ∈ Key)
7. ¬(key = u1 ∈ Key)
8. u2 : Value@i
9. v : (Key × Value) List@i
10. ↑lookup-list-map-inDom(deqKey;key;v) ⇐⇒ ↑isl(lookup-list-map-find(deqKey;key;v))@i
⊢ ↑rec-case(v) of [] => ff | h::t => r.let k,v = h in (deqKey key k) ∨br ⇐⇒ ↑isl(apply-alist(deqKey;v;key))

---

Latex:

---

Latex:

1.  Key  :  Type
2.  Value  :  Type
3.  deqKey  :  EqDecider(Key)
4.  key  :  Key
5.  u  :  Key  \mtimes{}  Value@i
6.  v  :  (Key  \mtimes{}  Value)  List@i
7.  \muparrow{}lookup-list-map-inDom(deqKey;key;v)  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}isl(lookup-list-map-find(deqKey;key;v))@i
\mvdash{}  \muparrow{}lookup-list-map-inDom(deqKey;key;[u  /  v])  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}isl(lookup-list-map-find(deqKey;key;[u  /  v]))


By

---

Latex:
(DProds
  THEN  RepUR  ``lookup-list-map-inDom  lookup-list-map-find  eqof``  0
  THEN  (BoolCase  \mkleeneopen{}deqKey  key  u1\mkleeneclose{}\mcdot{}  THEN  Try  (CpltAuto))
  THEN  BoolCase  \mkleeneopen{}deqKey  u1  key\mkleeneclose{}\mcdot{}
  THEN  Try  (CpltAuto))

---

Home Index