---

Step * 2 of Lemma last_induction


1. [T] : Type
2. [Q] : (T List) ⟶ ℙ
3. Q[[]]
4. ∀ys:T List. ∀y:T.  (Q[ys] ⇒ Q[ys @ [y]])
5. n : ℕ
6. zs : T List
7. ∀z1:T List. (||z1|| < ||zs|| ⇒ Q[z1])
8. ¬↑null(zs)
⊢ Q[zs]
BY
{ (((((FLemma `last_lemma` [(-1)]) THENA Auto)
     THEN ExRepD
     THEN (HypSubst (-1) 0)
     THEN Auto
     THEN BHyp 4
     THEN Auto
     THEN BackThruSomeHyp
     THEN Auto
     THEN (HypSubst (-1) 0))
   THENM RWO "length_append" 0
   )
   THEN Auto'
   ) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [Q]  :  (T  List)  {}\mrightarrow{}  \mBbbP{}
3.  Q[[]]
4.  \mforall{}ys:T  List.  \mforall{}y:T.    (Q[ys]  {}\mRightarrow{}  Q[ys  @  [y]])
5.  n  :  \mBbbN{}
6.  zs  :  T  List
7.  \mforall{}z1:T  List.  (||z1||  <  ||zs||  {}\mRightarrow{}  Q[z1])
8.  \mneg{}\muparrow{}null(zs)
\mvdash{}  Q[zs]


By

---

Latex:
(((((FLemma  `last\_lemma`  [(-1)])  THENA  Auto)
      THEN  ExRepD
      THEN  (HypSubst  (-1)  0)
      THEN  Auto
      THEN  BHyp  4
      THEN  Auto
      THEN  BackThruSomeHyp
      THEN  Auto
      THEN  (HypSubst  (-1)  0))
  THENM  RWO  "length\_append"  0
  )
  THEN  Auto'
  )

---

Home Index