---

Step * of Lemma map-sig-map-squash

∀[Key,Value:Type]. ∀[m:map-sig{i:l}(Key;Value)].  (↓map-sig-map(m))
BY
{ (Auto THEN D (-1) THEN Auto THEN D 0 THEN Unfold `map-sig-map` 0 THEN UseWitness ⌜m."empty"⌝⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Key,Value:Type].  \mforall{}[m:map-sig\{i:l\}(Key;Value)].    (\mdownarrow{}map-sig-map(m))


By

---

Latex:
(Auto
  THEN  D  (-1)
  THEN  Auto
  THEN  D  0
  THEN  Unfold  `map-sig-map`  0
  THEN  UseWitness  \mkleeneopen{}m."empty"\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index