---

Step * of Lemma select-upto

∀[m:ℕ]. ∀[n:ℕm].  (upto(m)[n] ~ n)
BY
{ (InstLemma `select_upto` [] THEN RepeatFor 2 (ParallelLast)) }

1
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

---

Latex:

---

Latex:
\mforall{}[m:\mBbbN{}].  \mforall{}[n:\mBbbN{}m].    (upto(m)[n]  \msim{}  n)


By

---

Latex:
(InstLemma  `select\_upto`  []  THEN  RepeatFor  2  (ParallelLast))

---

Home Index