---

Step * of Lemma firstn_last_mklist

∀[T:Type]. ∀[F:ℕ ⟶ T].  ∀n:ℕ+. (mklist(n;F) = (firstn(n - 1;mklist(n;F)) @ [last(mklist(n;F))]) ∈ (T List))
BY
{ (Auto THEN (Assert (n - 1) = (||mklist(n;F)|| - 1) ∈ ℕ BY (RWO "mklist_length" 0 THEN Auto)) THEN HypSubst' (-1) 0) }

1
1. T : Type
2. F : ℕ ⟶ T
3. n : ℕ+
4. (n - 1) = (||mklist(n;F)|| - 1) ∈ ℕ
⊢ mklist(n;F) = (firstn(||mklist(n;F)|| - 1;mklist(n;F)) @ [last(mklist(n;F))]) ∈ (T List)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[F:\mBbbN{}  {}\mrightarrow{}  T].    \mforall{}n:\mBbbN{}\msupplus{}.  (mklist(n;F)  =  (firstn(n  -  1;mklist(n;F))  @  [last(mklist(n;F))]))


By

---

Latex:
(Auto
  THEN  (Assert  (n  -  1)  =  (||mklist(n;F)||  -  1)  BY
                          (RWO  "mklist\_length"  0  THEN  Auto))
  THEN  HypSubst'  (-1)  0)

---

Home Index