---

Step * 1 of Lemma last-lemma-sq


1. T : Type
2. L : T List
3. ¬↑null(L)
⊢ L ~ firstn(||L|| - 1;L) @ [last(L)]
BY
{ Assert ⌜||L|| > 0⌝⋅ }

1
.....assertion..... 
1. T : Type
2. L : T List
3. ¬↑null(L)
⊢ ||L|| > 0

2
1. T : Type
2. L : T List
3. ¬↑null(L)
4. ||L|| > 0
⊢ L ~ firstn(||L|| - 1;L) @ [last(L)]

---

Latex:

---

Latex:

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


By

---

Latex:
Assert  \mkleeneopen{}||L||  >  0\mkleeneclose{}\mcdot{}

---

Home Index