---

Step * of Lemma firstn_last_mklist_sq

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

---

Latex:

---

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


By

---

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

---

Home Index