---

Step * 2 of Lemma co-regext-loopset


1. ∀t:coW(Unit;x.Unit). (regextfun(λp.loopset();t) ∈ coSet{i:l})
⊢ seteq(co-regext(loopset());loopset())
BY
{ Assert ⌜∀t:coW(Unit;x.Unit). (regextfun(λp.loopset();t) = loopset() ∈ coSet{i:l})⌝⋅ }

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

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})
⊢ seteq(co-regext(loopset());loopset())

---

Latex:

---

Latex:

1.  \mforall{}t:coW(Unit;x.Unit).  (regextfun(\mlambda{}p.loopset();t)  \mmember{}  coSet\{i:l\})
\mvdash{}  seteq(co-regext(loopset());loopset())


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}t:coW(Unit;x.Unit).  (regextfun(\mlambda{}p.loopset();t)  =  loopset())\mkleeneclose{}\mcdot{}

---

Home Index