---

Step * 2 2 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})
⊢ seteq(co-regext(loopset());loopset())
BY
{ ((Assert co-regext(loopset()) ~ mk-coset(coW(Unit;x.Unit);λw.regextfun(λp.loopset();w)) BY
          (RW (SubC (TagC (mk_tag_term 0))) 0 THEN Auto THEN Computation))
   THEN (BLemma `co-seteq-iff` THENA Auto)
   THEN RWO "setmem-loopset" 0
   THEN Auto
   THEN All (\h. RWO "3" h THEN SetMemDef h)
   THEN ((RWO "2" (-1) THEN Auto) ORELSE (RWO "2" 0 THEN Auto))) }

1
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})
3. co-regext(loopset()) ~ mk-coset(coW(Unit;x.Unit);λw.regextfun(λp.loopset();w))
4. z : coSet{i:l}@i'
5. seteq(z;loopset())
⊢ ∃t:coW(Unit;x.Unit). seteq(z;loopset())

---

Latex:

---

Latex:

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


By

---

Latex:
((Assert  co-regext(loopset())  \msim{}  mk-coset(coW(Unit;x.Unit);\mlambda{}w.regextfun(\mlambda{}p.loopset();w))  BY
                (RW  (SubC  (TagC  (mk\_tag\_term  0)))  0  THEN  Auto  THEN  Computation))
  THEN  (BLemma  `co-seteq-iff`  THENA  Auto)
  THEN  RWO  "setmem-loopset"  0
  THEN  Auto
  THEN  All  (\mbackslash{}h.  RWO  "3"  h  THEN  SetMemDef  h)
  THEN  ((RWO  "2"  (-1)  THEN  Auto)  ORELSE  (RWO  "2"  0  THEN  Auto)))

---

Home Index