---

Step * of Lemma length_upto

∀[n:ℕ]. (||upto(n)|| ~ n)
BY
{ (Unfold `upto` 0 THEN (D 0 THENA Auto)) }

1
1. n : ℕ
⊢ ||[0, n)|| ~ n

---

Latex:

---

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


By

---

Latex:
(Unfold  `upto`  0  THEN  (D  0  THENA  Auto))

---

Home Index