---

Step * of Lemma test-mutual-corec-size_wf

∀[i:ℕ2]. ∀[x:test-mutual-corec() i].  (test-mutual-corec-size(i;x) ∈ partial(ℕ))
BY
{ ProveMutualCorecSizeWf⋅ }

---

Latex:

---

Latex:
\mforall{}[i:\mBbbN{}2].  \mforall{}[x:test-mutual-corec()  i].    (test-mutual-corec-size(i;x)  \mmember{}  partial(\mBbbN{}))


By

---

Latex:
ProveMutualCorecSizeWf\mcdot{}

---

Home Index