---

Step * of Lemma lookup-list-map-inDom_wf

∀[Key,Value:Type]. ∀[deqKey:EqDecider(Key)]. ∀[key:Key]. ∀[m:lookup-list-map-type(Key;Value)].
  (lookup-list-map-inDom(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;[]) ∈ 𝔹

---

Latex:


\mforall{}[Key,Value:Type].  \mforall{}[deqKey:EqDecider(Key)].  \mforall{}[key:Key].  \mforall{}[m:lookup-list-map-type(Key;Value)].
    (lookup-list-map-inDom(deqKey;key;m)  \mmember{}  \mBbbB{})


By

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

---

Home Index