---

Step * of Lemma firstn_last

∀[T:Type]. ∀[L:T List].  L = (firstn(||L|| - 1;L) @ [last(L)]) ∈ (T List) supposing ¬↑null(L)
BY
{ TACTIC:(InductionOnList THEN Reduce 0 THEN Auto THEN Try (((D (-1)) THEN Trivial))) }

1
1. T : Type
2. u : T
3. v : T List
4. v = (firstn(||v|| - 1;v) @ [last(v)]) ∈ (T List) supposing ¬↑null(v)
5. ¬False
⊢ [u / v] = (firstn((||v|| + 1) - 1;[u / v]) @ [last([u / v])]) ∈ (T List)

---

Latex:

---

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


By

---

Latex:
TACTIC:(InductionOnList  THEN  Reduce  0  THEN  Auto  THEN  Try  (((D  (-1))  THEN  Trivial)))

---

Home Index