---

Step * of Lemma map-sig-update_wf

∀[Key,Value:Type]. ∀[m:map-sig{i:l}(Key;Value)].  (map-sig-update(m) ∈ Key ─→ Value ─→ map-sig-map(m) ─→ map-sig-map(m))
BY
{ (ProveWfLemma THEN Unfold `map-sig-map` 0 THEN D (-1) THEN Auto) }

---

Latex:


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


By

(ProveWfLemma  THEN  Unfold  `map-sig-map`  0  THEN  D  (-1)  THEN  Auto)

---

Home Index