---

Step * 2 1 1 1 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)
3. T : 𝕌'
4. (a:Type × (a ⟶ T)) ⊆r T
5. coSet{i:l} ⊆r T
6. regextfun(λp.loopset();t) = loopset() ∈ T
⊢ regextfun(λp.loopset();t) = loopset() ∈ (a:Type × (a ⟶ T))
BY
{ (RW (AddrC [3] (LemmaC `loopset-sq`)) 0
   THEN coWD 2
   THEN D 2
   THEN RecUnfold `regextfun` 0
   THEN RepUR ``mk-set Wsup mk-coset`` 0
   THEN EqCDA) }

1
.....subterm..... T:t
1:n
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
⊢ set-dom(loopset()) = Unit ∈ Type

2
.....subterm..... T:t
2:n
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
⊢ (λu.regextfun(λp.loopset();t1 u)) = (λp.loopset()) ∈ (set-dom(loopset()) ⟶ T)

---

Latex:

---

Latex:

1.  \mforall{}t:coW(Unit;x.Unit).  (regextfun(\mlambda{}p.loopset();t)  \mmember{}  coSet\{i:l\})
2.  t  :  coW(Unit;x.Unit)
3.  T  :  \mBbbU{}'
4.  (a:Type  \mtimes{}  (a  {}\mrightarrow{}  T))  \msubseteq{}r  T
5.  coSet\{i:l\}  \msubseteq{}r  T
6.  regextfun(\mlambda{}p.loopset();t)  =  loopset()
\mvdash{}  regextfun(\mlambda{}p.loopset();t)  =  loopset()


By

---

Latex:
(RW  (AddrC  [3]  (LemmaC  `loopset-sq`))  0
  THEN  coWD  2
  THEN  D  2
  THEN  RecUnfold  `regextfun`  0
  THEN  RepUR  ``mk-set  Wsup  mk-coset``  0
  THEN  EqCDA)

---

Home Index