---

Step * of Lemma last_lemma

∀[T:Type]. ∀L:T List. ∃L':T List. (L = (L' @ [last(L)]) ∈ (T List)) supposing ¬↑null(L)
BY
{ TACTIC:(Auto THEN With ⌜firstn(||L|| - 1;L)⌝ (D 0)⋅ THEN Auto) }

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

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}L:T  List.  \mexists{}L':T  List.  (L  =  (L'  @  [last(L)]))  supposing  \mneg{}\muparrow{}null(L)


By

---

Latex:
TACTIC:(Auto  THEN  With  \mkleeneopen{}firstn(||L||  -  1;L)\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index