---

Step * of Lemma co-regext_wf

∀[a:coSet{i:l}]. (co-regext(a) ∈ coSet{i:l})
BY
{ (Auto THEN (coSetD 1 THEN D 1) THEN RepUR ``co-regext`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[a:coSet\{i:l\}].  (co-regext(a)  \mmember{}  coSet\{i:l\})


By

---

Latex:
(Auto  THEN  (coSetD  1  THEN  D  1)  THEN  RepUR  ``co-regext``  0  THEN  Auto)

---

Home Index