---

Step * of Lemma set-sig-empty-prop

∀[Item:Type]. ∀[s:set-sig{i:l}(Item)]. ∀[x:Item].  (¬↑(set-sig-member(s) x set-sig-empty(s)))
BY
{ (Auto
   THEN (Assert ⌜s ∈ set-sig{i:l}(Item)⌝⋅ THENA Auto)
   THEN (D 2 THENA Auto)
   THEN All(Folds ``set-sig-member set-sig-empty set-sig-set``)
   THEN DVarSets
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Item:Type].  \mforall{}[s:set-sig\{i:l\}(Item)].  \mforall{}[x:Item].    (\mneg{}\muparrow{}(set-sig-member(s)  x  set-sig-empty(s)))


By

---

Latex:
(Auto
  THEN  (Assert  \mkleeneopen{}s  \mmember{}  set-sig\{i:l\}(Item)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (D  2  THENA  Auto)
  THEN  All(Folds  ``set-sig-member  set-sig-empty  set-sig-set``)
  THEN  DVarSets
  THEN  Auto)

---

Home Index