---

Step * of Lemma from-upto-is-singleton

∀[n,m:ℤ].  [n, m) = [n] ∈ (ℤ List) supposing m = (n + 1) ∈ ℤ
BY
{ (Auto
   THEN (HypSubst' (-1) 0 THENA Auto)
   THEN RecUnfold `from-upto` 0
   THEN AutoSplit
   THEN CallByValueReduce 0
   THEN Auto
   THEN RWO "from-upto-nil" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[n,m:\mBbbZ{}].    [n,  m)  =  [n]  supposing  m  =  (n  +  1)


By

---

Latex:
(Auto
  THEN  (HypSubst'  (-1)  0  THENA  Auto)
  THEN  RecUnfold  `from-upto`  0
  THEN  AutoSplit
  THEN  CallByValueReduce  0
  THEN  Auto
  THEN  RWO  "from-upto-nil"  0
  THEN  Auto)

---

Home Index