---

Step * of Lemma map-sig-inDom-prop

∀[Key,Value:Type]. ∀[ms:map-sig{i:l}(Key;Value)]. ∀[k:Key]. ∀[m:map-sig-map(ms)].
  (↑(map-sig-inDom(ms) k m) ⇐⇒ ↑isl(map-sig-find(ms) k m))
BY
{ ((UnivCD THENA Auto)
   THEN (Assert ⌈ms ∈ map-sig{i:l}(Key;Value)⌉⋅ THENA Auto)
   THEN (D 3 THENA Auto)
   THEN DVarSets
   THEN (Unhide THENA Auto)
   THEN All (Folds ``map-sig-inDom map-sig-map map-sig-find``)
   THEN Auto) }

---

Latex:


\mforall{}[Key,Value:Type].  \mforall{}[ms:map-sig\{i:l\}(Key;Value)].  \mforall{}[k:Key].  \mforall{}[m:map-sig-map(ms)].
    (\muparrow{}(map-sig-inDom(ms)  k  m)  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}isl(map-sig-find(ms)  k  m))


By

((UnivCD  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}ms  \mmember{}  map-sig\{i:l\}(Key;Value)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (D  3  THENA  Auto)
  THEN  DVarSets
  THEN  (Unhide  THENA  Auto)
  THEN  All  (Folds  ``map-sig-inDom  map-sig-map  map-sig-find``)
  THEN  Auto)

---

Home Index