---

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

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

1
1. Key : Type
2. Value : Type
3. deqKey : EqDecider(Key)
⊢ ↑lookup-list-map-isEmpty([]) ⇐⇒ ∀k:Key. (¬↑lookup-list-map-inDom(deqKey;k;[]))

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

---

Latex:

---

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


By

---

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

---

Home Index