---

Step * of Lemma map-sig-map-vatype

∀[Key,Value:Type]. ∀[m:map-sig{i:l}(Key;Value)].
  (valueall-type(map-sig-map(m))) supposing (valueall-type(Key) and valueall-type(Value))
BY
{ (Auto THEN D (-3) THEN Try (Complete ((Unfold `map-sig-map` 0 THEN DVarSets THEN Unhide THEN Auto))) THEN Auto) }

---

Latex:


\mforall{}[Key,Value:Type].  \mforall{}[m:map-sig\{i:l\}(Key;Value)].
    (valueall-type(map-sig-map(m)))  supposing  (valueall-type(Key)  and  valueall-type(Value))


By

(Auto
  THEN  D  (-3)
  THEN  Try  (Complete  ((Unfold  `map-sig-map`  0  THEN  DVarSets  THEN  Unhide  THEN  Auto)))
  THEN  Auto)

---

Home Index