---

Step * 2 2 1 of Lemma co-regext-loopset


1. ∀t:coW(Unit;x.Unit). (regextfun(λp.loopset();t) ∈ coSet{i:l})
2. ∀t:coW(Unit;x.Unit). (regextfun(λp.loopset();t) = loopset() ∈ coSet{i:l})
3. co-regext(loopset()) ~ mk-coset(coW(Unit;x.Unit);λw.regextfun(λp.loopset();w))
4. z : coSet{i:l}@i'
5. seteq(z;loopset())
⊢ ∃t:coW(Unit;x.Unit). seteq(z;loopset())
BY
{ Assert ⌜coW(Unit;x.Unit)⌝⋅ }

1
.....assertion..... 
1. ∀t:coW(Unit;x.Unit). (regextfun(λp.loopset();t) ∈ coSet{i:l})
2. ∀t:coW(Unit;x.Unit). (regextfun(λp.loopset();t) = loopset() ∈ coSet{i:l})
3. co-regext(loopset()) ~ mk-coset(coW(Unit;x.Unit);λw.regextfun(λp.loopset();w))
4. z : coSet{i:l}@i'
5. seteq(z;loopset())
⊢ coW(Unit;x.Unit)

2
1. ∀t:coW(Unit;x.Unit). (regextfun(λp.loopset();t) ∈ coSet{i:l})
2. ∀t:coW(Unit;x.Unit). (regextfun(λp.loopset();t) = loopset() ∈ coSet{i:l})
3. co-regext(loopset()) ~ mk-coset(coW(Unit;x.Unit);λw.regextfun(λp.loopset();w))
4. z : coSet{i:l}@i'
5. seteq(z;loopset())
6. coW(Unit;x.Unit)
⊢ ∃t:coW(Unit;x.Unit). seteq(z;loopset())

---

Latex:

---

Latex:

1.  \mforall{}t:coW(Unit;x.Unit).  (regextfun(\mlambda{}p.loopset();t)  \mmember{}  coSet\{i:l\})
2.  \mforall{}t:coW(Unit;x.Unit).  (regextfun(\mlambda{}p.loopset();t)  =  loopset())
3.  co-regext(loopset())  \msim{}  mk-coset(coW(Unit;x.Unit);\mlambda{}w.regextfun(\mlambda{}p.loopset();w))
4.  z  :  coSet\{i:l\}@i'
5.  seteq(z;loopset())
\mvdash{}  \mexists{}t:coW(Unit;x.Unit).  seteq(z;loopset())


By

---

Latex:
Assert  \mkleeneopen{}coW(Unit;x.Unit)\mkleeneclose{}\mcdot{}

---

Home Index