---

Step * 1 of Lemma co-regext-loopset

.....assertion..... 
∀t:coW(Unit;x.Unit). (regextfun(λp.loopset();t) ∈ coSet{i:l})
BY
{ (Intro THEN (InstLemma `regextfun_wf` [⌜Unit⌝;⌜λp.loopset()⌝]⋅ THENA Auto)) }

1
1. t : coW(Unit;x.Unit)@i
2. ∀[w:coW(Unit;x.set-dom((λp.loopset()) x))]. (regextfun(λp.loopset();w) ∈ coSet{i:l})
⊢ regextfun(λp.loopset();t) ∈ coSet{i:l}

---

Latex:

---

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


By

---

Latex:
(Intro  THEN  (InstLemma  `regextfun\_wf`  [\mkleeneopen{}Unit\mkleeneclose{};\mkleeneopen{}\mlambda{}p.loopset()\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index