---

Step * of Lemma map-sig-eqKey_wf

∀[Key,Value:Type]. ∀[m:map-sig{i:l}(Key;Value)].  (map-sig-eqKey(m) ∈ EqDecider(Key))
BY
{ (ProveWfLemma THEN D (-1) THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(ProveWfLemma  THEN  D  (-1)  THEN  Auto)

---

Home Index