---

Step * of Lemma set-sig-set-vatype

∀[Item:Type]. ∀[s:set-sig{i:l}(Item)].  valueall-type(set-sig-set(s)) supposing valueall-type(Item)
BY
{ (Auto THEN D (-2) THEN Try (Complete ((Unfold `set-sig-set` 0 THEN DVarSets THEN Unhide THEN Auto))) THEN Auto) }

---

Latex:


\mforall{}[Item:Type].  \mforall{}[s:set-sig\{i:l\}(Item)].    valueall-type(set-sig-set(s))  supposing  valueall-type(Item)


By

(Auto
  THEN  D  (-2)
  THEN  Try  (Complete  ((Unfold  `set-sig-set`  0  THEN  DVarSets  THEN  Unhide  THEN  Auto)))
  THEN  Auto)

---

Home Index