---

Step * of Lemma set-sig-empty-prop2

∀[Item:Type]. ∀[s:set-sig{i:l}(Item)]. ∀[x:Item].  uiff(↑(set-sig-member(s) x set-sig-empty(s));False)
BY
{ (Auto THEN InstLemma `set-sig-empty-prop` [⌈Item⌉;⌈s⌉;⌈x⌉]⋅ THEN Auto) }

---

Latex:


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


By

(Auto  THEN  InstLemma  `set-sig-empty-prop`  [\mkleeneopen{}Item\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index