---

Step * 1 2 1 of Lemma last-lemma-sq

.....equality..... 
1. T : Type
2. L : T List
3. ¬↑null(L)
4. ||L|| > 0
⊢ [last(L)] ~ nth_tl(||L|| - 1;L)
BY
{ ((InstLemma `list_decomp` [T; nth_tl(||L|| - 1;L)])⋅ THENA Auto) }

1
1. T : Type
2. L : T List
3. ¬↑null(L)
4. ||L|| > 0
5. nth_tl(||L|| - 1;L) ~ [hd(nth_tl(||L|| - 1;L)) / tl(nth_tl(||L|| - 1;L))]
⊢ [last(L)] ~ nth_tl(||L|| - 1;L)

---

Latex:

---

Latex:
.....equality..... 
1.  T  :  Type
2.  L  :  T  List
3.  \mneg{}\muparrow{}null(L)
4.  ||L||  >  0
\mvdash{}  [last(L)]  \msim{}  nth\_tl(||L||  -  1;L)


By

---

Latex:
((InstLemma  `list\_decomp`  [T;  nth\_tl(||L||  -  1;L)])\mcdot{}  THENA  Auto)

---

Home Index