---

Step * 2 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)
⊢ regextfun(λp.loopset();t) = loopset() ∈ coSet{i:l}
BY
{ ((BLemma `coSet-equality2` THENW Auto) THEN RepeatFor 2 (Intro)) }

1
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) ∧ (coSet{i:l} ⊆r T)
⊢ (regextfun(λp.loopset();t) = loopset() ∈ T) ⇒ (regextfun(λp.loopset();t) = loopset() ∈ (a:Type × (a ⟶ 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)
\mvdash{}  regextfun(\mlambda{}p.loopset();t)  =  loopset()


By

---

Latex:
((BLemma  `coSet-equality2`  THENW  Auto)  THEN  RepeatFor  2  (Intro))

---

Home Index