---

Step * 1 of Lemma regext-loopset-empty


1. regext(loopset()) ~ mk-coset(W(Unit;x.Unit);λw.regextfun(λp.loopset();w))
⊢ seteq(regext(loopset());{})
BY
{ ((BLemma `co-seteq-iff` THENA Auto) THEN Intro THEN RWO "setmem-emptyset" 0 THEN Auto) }

1
1. regext(loopset()) ~ mk-coset(W(Unit;x.Unit);λw.regextfun(λp.loopset();w))
2. z : coSet{i:l}
3. (z ∈ regext(loopset()))
⊢ False

---

Latex:

---

Latex:

1.  regext(loopset())  \msim{}  mk-coset(W(Unit;x.Unit);\mlambda{}w.regextfun(\mlambda{}p.loopset();w))
\mvdash{}  seteq(regext(loopset());\{\})


By

---

Latex:
((BLemma  `co-seteq-iff`  THENA  Auto)  THEN  Intro  THEN  RWO  "setmem-emptyset"  0  THEN  Auto)

---

Home Index