---

Step * 2 1 of Lemma co-regext-loopset

.....assertion..... 
1. ∀t:coW(Unit;x.Unit). (regextfun(λp.loopset();t) ∈ coSet{i:l})
⊢ ∀t:coW(Unit;x.Unit). (regextfun(λp.loopset();t) = loopset() ∈ coSet{i:l})
BY
{ Intro }

1
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}

---

Latex:

---

Latex:
.....assertion..... 
1.  \mforall{}t:coW(Unit;x.Unit).  (regextfun(\mlambda{}p.loopset();t)  \mmember{}  coSet\{i:l\})
\mvdash{}  \mforall{}t:coW(Unit;x.Unit).  (regextfun(\mlambda{}p.loopset();t)  =  loopset())


By

---

Latex:
Intro

---

Home Index