---

Step * 1 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
{ (DVar `zs' THEN All Reduce 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.  \muparrow{}null(zs)
\mvdash{}  Q[zs]


By

---

Latex:
(DVar  `zs'  THEN  All  Reduce  THEN  Auto)

---

Home Index