---

Step * of Lemma nat2inf-one-one

∀[a,b:ℕ].  ((a∞ = b∞ ∈ ℕ∞) ⇒ (a = b ∈ ℕ))
BY
{ (Auto
   THEN RepUR ``nat2inf`` -1
   THEN (ApFunToHypEquands `F' ⌜F a⌝ ⌜𝔹⌝ (-1)⋅ THENA Auto)
   THEN (Reduce (-1)
         THEN (Assert ¬↑a <z b BY
                     (RevHypSubst' (-1) 0 THEN RW assert_pushdownC 0 THEN Auto))
         THEN Thin (-2)
         THEN (RW assert_pushdownC (-1) THENA Auto))
   THEN (ApFunToHypEquands `F' ⌜F b⌝ ⌜𝔹⌝ (-2)⋅ THENA Auto)
   THEN (Reduce (-1)
         THEN (Assert ¬↑b <z a BY
                     (HypSubst' (-1) 0 THEN RW assert_pushdownC 0 THEN Auto))
         THEN Thin (-2)
         THEN (RW assert_pushdownC (-1) THENA Auto))
   THEN Auto') }

---

Latex:

---

Latex:
\mforall{}[a,b:\mBbbN{}].    ((a\minfty{}  =  b\minfty{})  {}\mRightarrow{}  (a  =  b))


By

---

Latex:
(Auto
  THEN  RepUR  ``nat2inf``  -1
  THEN  (ApFunToHypEquands  `F'  \mkleeneopen{}F  a\mkleeneclose{}  \mkleeneopen{}\mBbbB{}\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)
  THEN  (Reduce  (-1)
              THEN  (Assert  \mneg{}\muparrow{}a  <z  b  BY
                                      (RevHypSubst'  (-1)  0  THEN  RW  assert\_pushdownC  0  THEN  Auto))
              THEN  Thin  (-2)
              THEN  (RW  assert\_pushdownC  (-1)  THENA  Auto))
  THEN  (ApFunToHypEquands  `F'  \mkleeneopen{}F  b\mkleeneclose{}  \mkleeneopen{}\mBbbB{}\mkleeneclose{}  (-2)\mcdot{}  THENA  Auto)
  THEN  (Reduce  (-1)
              THEN  (Assert  \mneg{}\muparrow{}b  <z  a  BY
                                      (HypSubst'  (-1)  0  THEN  RW  assert\_pushdownC  0  THEN  Auto))
              THEN  Thin  (-2)
              THEN  (RW  assert\_pushdownC  (-1)  THENA  Auto))
  THEN  Auto')

---

Home Index