---

Step * 1 1 of Lemma last_lemma


1. T : Type
2. L : T List
3. ¬↑null(L)
⊢ ||L|| = (||firstn(||L|| - 1;L)|| + 1) ∈ ℤ
BY
{ (RWW "length_append length_firstn" 0 THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  L  :  T  List
3.  \mneg{}\muparrow{}null(L)
\mvdash{}  ||L||  =  (||firstn(||L||  -  1;L)||  +  1)


By

---

Latex:
(RWW  "length\_append  length\_firstn"  0  THEN  Reduce  0  THEN  Auto)

---

Home Index