---

Step * of Lemma equal-nat-inf-infinity2

∀[x:ℕ∞]. uiff(x = ∞ ∈ ℕ∞;∀i:ℕ. (↑(x i)))
BY
{ (Auto THEN HypSubst' (-2) 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[x:\mBbbN{}\minfty{}].  uiff(x  =  \minfty{};\mforall{}i:\mBbbN{}.  (\muparrow{}(x  i)))


By

---

Latex:
(Auto  THEN  HypSubst'  (-2)  0  THEN  Auto)

---

Home Index