---

Step * 1 of Lemma select-upto


1. ∀[m:ℕ]. ∀[n:ℕm].  (upto(m)[n] = n ∈ ℤ)
2. [m] : ℕ
3. ∀[n:ℕm]. (upto(m)[n] = n ∈ ℤ)
4. [n] : ℕm
5. upto(m)[n] = n ∈ ℤ
⊢ upto(m)[n] ~ n
BY
{ (HypSubst' (-1) 0 THEN Auto) }

---

Latex:

---

Latex:

1.  \mforall{}[m:\mBbbN{}].  \mforall{}[n:\mBbbN{}m].    (upto(m)[n]  =  n)
2.  [m]  :  \mBbbN{}
3.  \mforall{}[n:\mBbbN{}m].  (upto(m)[n]  =  n)
4.  [n]  :  \mBbbN{}m
5.  upto(m)[n]  =  n
\mvdash{}  upto(m)[n]  \msim{}  n


By

---

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

---

Home Index