---

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

.....assertion..... 
1. ∀t:coW(Unit;x.Unit). (regextfun(λp.loopset();t) ∈ coSet{i:l})
2. x : Unit
3. t1 : Unit ⟶ coW(Unit;x.Unit)
4. T : 𝕌'
5. (a:Type × (a ⟶ T)) ⊆r T
6. coSet{i:l} ⊆r T
7. regextfun(λp.loopset();<x, t1>) = loopset() ∈ T
8. u : set-dom(loopset())
⊢ regextfun(λp.loopset();<x, t1>) = regextfun(λp.loopset();t1 u) ∈ T
BY
{ Assert ⌜<x, t1> = (t1 u) ∈ coW(Unit;x.Unit)⌝⋅ }

1
.....assertion..... 
1. ∀t:coW(Unit;x.Unit). (regextfun(λp.loopset();t) ∈ coSet{i:l})
2. x : Unit
3. t1 : Unit ⟶ coW(Unit;x.Unit)
4. T : 𝕌'
5. (a:Type × (a ⟶ T)) ⊆r T
6. coSet{i:l} ⊆r T
7. regextfun(λp.loopset();<x, t1>) = loopset() ∈ T
8. u : set-dom(loopset())
⊢ <x, t1> = (t1 u) ∈ coW(Unit;x.Unit)

2
1. ∀t:coW(Unit;x.Unit). (regextfun(λp.loopset();t) ∈ coSet{i:l})
2. x : Unit
3. t1 : Unit ⟶ coW(Unit;x.Unit)
4. T : 𝕌'
5. (a:Type × (a ⟶ T)) ⊆r T
6. coSet{i:l} ⊆r T
7. regextfun(λp.loopset();<x, t1>) = loopset() ∈ T
8. u : set-dom(loopset())
9. <x, t1> = (t1 u) ∈ coW(Unit;x.Unit)
⊢ regextfun(λp.loopset();<x, t1>) = regextfun(λp.loopset();t1 u) ∈ T

---

Latex:

---

Latex:
.....assertion..... 
1.  \mforall{}t:coW(Unit;x.Unit).  (regextfun(\mlambda{}p.loopset();t)  \mmember{}  coSet\{i:l\})
2.  x  :  Unit
3.  t1  :  Unit  {}\mrightarrow{}  coW(Unit;x.Unit)
4.  T  :  \mBbbU{}'
5.  (a:Type  \mtimes{}  (a  {}\mrightarrow{}  T))  \msubseteq{}r  T
6.  coSet\{i:l\}  \msubseteq{}r  T
7.  regextfun(\mlambda{}p.loopset();<x,  t1>)  =  loopset()
8.  u  :  set-dom(loopset())
\mvdash{}  regextfun(\mlambda{}p.loopset();<x,  t1>)  =  regextfun(\mlambda{}p.loopset();t1  u)


By

---

Latex:
Assert  \mkleeneopen{}<x,  t1>  =  (t1  u)\mkleeneclose{}\mcdot{}

---

Home Index