---

Step * of Lemma co-value-ext

co-value() ≡ atomic-values() ⋃ (co-value() × co-value()) ⋃ (co-value() + co-value())
BY
{ ProveCoDatatypeExt⋅ }

---

Latex:

---

Latex:
co-value()  \mequiv{}  atomic-values()  \mcup{}  (co-value()  \mtimes{}  co-value())  \mcup{}  (co-value()  +  co-value())


By

---

Latex:
ProveCoDatatypeExt\mcdot{}

---

Home Index