---

Step * 1 of Lemma last_lemma


1. T : Type
2. L : T List
3. ¬↑null(L)
⊢ L = (firstn(||L|| - 1;L) @ [last(L)]) ∈ (T List)
BY
{ (BLemma `list_extensionality` THEN Auto) }

1
1. T : Type
2. L : T List
3. ¬↑null(L)
⊢ ||L|| = (||firstn(||L|| - 1;L)|| + 1) ∈ ℤ

2
1. T : Type
2. L : T List
3. ¬↑null(L)
4. i : ℕ
5. i < ||L||
⊢ L[i] = firstn(||L|| - 1;L) @ [last(L)][i] ∈ T

---

Latex:

---

Latex:

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


By

---

Latex:
(BLemma  `list\_extensionality`  THEN  Auto)

---

Home Index