---

Step * of Lemma set-sig-set-squash

∀[Item:Type]. ∀[s:set-sig{i:l}(Item)].  (↓set-sig-set(s))
BY
{ (Auto THEN D (-1) THEN Auto THEN D 0 THEN Unfold `set-sig-set` 0 THEN UseWitness ⌈s."empty"⌉⋅ THEN Auto) }

---

Latex:


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


By

(Auto
  THEN  D  (-1)
  THEN  Auto
  THEN  D  0
  THEN  Unfold  `set-sig-set`  0
  THEN  UseWitness  \mkleeneopen{}s."empty"\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index