---

Step * of Lemma lastn-nil

∀[n:ℤ]. (lastn(n;[]) ~ [])
BY
{ xxx((D 0 THENA Auto)
      THEN (RWO "lastn-cases" 0 THENA Auto)
      THEN Reduce 0
      THEN RepeatFor 2 (((SplitOnConclITE THENA Auto) THEN Try (Trivial))))xxx }

1
.....falsecase..... 
1. n : ℤ
2. n < 0
3. 0 < n
⊢ lastn(n;[]) ~ []

---

Latex:

---

Latex:
\mforall{}[n:\mBbbZ{}].  (lastn(n;[])  \msim{}  [])


By

---

Latex:
xxx((D  0  THENA  Auto)
        THEN  (RWO  "lastn-cases"  0  THENA  Auto)
        THEN  Reduce  0
        THEN  RepeatFor  2  (((SplitOnConclITE  THENA  Auto)  THEN  Try  (Trivial))))xxx

---

Home Index