---

Step * of Lemma upto_equal_nil

∀[n:ℕ]. uiff(upto(n) = [] ∈ (ℤ List);n = 0 ∈ ℤ)
BY
{ (Auto
   THEN Try ((FLemma `equal-nil-sq-nil` [-1] THENA Auto))
   THEN Try ((BLemma `upto_is_nil` THEN Auto))
   THEN Try (((FLemma `upto_is_nil`[-1] THENM HypSubst' -1 0) THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  uiff(upto(n)  =  [];n  =  0)


By

---

Latex:
(Auto
  THEN  Try  ((FLemma  `equal-nil-sq-nil`  [-1]  THENA  Auto))
  THEN  Try  ((BLemma  `upto\_is\_nil`  THEN  Auto))
  THEN  Try  (((FLemma  `upto\_is\_nil`[-1]  THENM  HypSubst'  -1  0)  THEN  Auto)))

---

Home Index