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 (-2) THEN Try (Complete ((Unfold `set-sig-set` 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