---

Step * 1 1 of Lemma regext-loopset-empty


1. regext(loopset()) ~ mk-coset(W(Unit;x.Unit);λw.regextfun(λp.loopset();w))
2. z : coSet{i:l}
3. (z ∈ regext(loopset()))
⊢ False
BY
{ (RWO "1" (-1) THEN SetMemDef (-1) THEN ThinVar `z' THEN Thin 1) }

1
1. t : W(Unit;x.Unit)
⊢ False

---

Latex:

---

Latex:

1.  regext(loopset())  \msim{}  mk-coset(W(Unit;x.Unit);\mlambda{}w.regextfun(\mlambda{}p.loopset();w))
2.  z  :  coSet\{i:l\}
3.  (z  \mmember{}  regext(loopset()))
\mvdash{}  False


By

---

Latex:
(RWO  "1"  (-1)  THEN  SetMemDef  (-1)  THEN  ThinVar  `z'  THEN  Thin  1)

---

Home Index