---

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

∀[Key,Value:Type]. ∀[deqKey:EqDecider(Key)]. ∀[key2:Key]. ∀[m:lookup-list-map-type(Key;Value)]. ∀[key1:Key].
  (lookup-list-map-find(deqKey;key1;lookup-list-map-remove(deqKey;key2;m))
  = if deqKey key1 key2 then inr ⋅  else lookup-list-map-find(deqKey;key1;m) fi 
  ∈ (Value?))
BY
{ ((UnivCD THENA Auto) THEN RepUR ``lookup-list-map-type`` (-2) THEN ListInd (-2)⋅ THEN AllReduce THEN Try (CpltAuto)) }

1
1. Key : Type
2. Value : Type
3. deqKey : EqDecider(Key)
4. key2 : Key
5. key1 : Key
6. u : Key × Value@i
7. v : (Key × Value) List@i
8. lookup-list-map-find(deqKey;key1;lookup-list-map-remove(deqKey;key2;v))
= if deqKey key1 key2 then inr ⋅  else lookup-list-map-find(deqKey;key1;v) fi 
∈ (Value?)@i
⊢ lookup-list-map-find(deqKey;key1;lookup-list-map-remove(deqKey;key2;[u / v]))
= if deqKey key1 key2 then inr ⋅  else lookup-list-map-find(deqKey;key1;[u / v]) fi 
∈ (Value?)

---

Latex:

---

Latex:
\mforall{}[Key,Value:Type].  \mforall{}[deqKey:EqDecider(Key)].  \mforall{}[key2:Key].  \mforall{}[m:lookup-list-map-type(Key;Value)].
\mforall{}[key1:Key].
    (lookup-list-map-find(deqKey;key1;lookup-list-map-remove(deqKey;key2;m))
    =  if  deqKey  key1  key2  then  inr  \mcdot{}    else  lookup-list-map-find(deqKey;key1;m)  fi  )


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RepUR  ``lookup-list-map-type``  (-2)
  THEN  ListInd  (-2)\mcdot{}
  THEN  AllReduce
  THEN  Try  (CpltAuto))

---

Home Index