---

Step * 2 of Lemma equal-nat-inf-infinity


1. x : ℕ∞
2. ∀i:ℕ. (¬(x = i∞ ∈ ℕ∞))
⊢ x = ∞ ∈ ℕ∞
BY
{ (D 1
   THEN EqTypeCD
   THEN Auto
   THEN Ext
   THEN Auto
   THEN RenameVar `n' (-1)
   THEN RepUR ``nat-inf-infinity`` 0
   THEN CompNatInd (-1)
   THEN SimpleBoolCase ⌜x n⌝⋅
   THEN Auto) }

1
1. x : ℕ ⟶ 𝔹
2. ∀n:ℕ. ((↑(x (n + 1))) ⇒ (↑(x n)))
3. ∀i:ℕ. (¬(x = i∞ ∈ ℕ∞))
4. n : ℕ
5. ∀n:ℕn. x n = tt
6. x n = ff
⊢ ff = tt

---

Latex:

---

Latex:

1.  x  :  \mBbbN{}\minfty{}
2.  \mforall{}i:\mBbbN{}.  (\mneg{}(x  =  i\minfty{}))
\mvdash{}  x  =  \minfty{}


By

---

Latex:
(D  1
  THEN  EqTypeCD
  THEN  Auto
  THEN  Ext
  THEN  Auto
  THEN  RenameVar  `n'  (-1)
  THEN  RepUR  ``nat-inf-infinity``  0
  THEN  CompNatInd  (-1)
  THEN  SimpleBoolCase  \mkleeneopen{}x  n\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index