---

Step * 1 of Lemma length_upto


1. n : ℕ
⊢ ||[0, n)|| ~ n
BY
{ ((RWO "length-from-upto" 0⋅ THEN Auto) THEN AutoSplit) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
\mvdash{}  ||[0,  n)||  \msim{}  n


By

---

Latex:
((RWO  "length-from-upto"  0\mcdot{}  THEN  Auto)  THEN  AutoSplit)

---

Home Index