---

Step * 1 1 of Lemma last_induction_accum


1. T : Type
2. Q : (T List) ⟶ ℙ
3. base : Q[[]]
4. step : ∀[ys:T List]. (Q[ys] ⇒ (∀y:T. Q[ys @ [y]]))
⊢ base ∈ Q[[]]
BY
{ Auto }

---

Latex:

---

Latex:

1.  T  :  Type
2.  Q  :  (T  List)  {}\mrightarrow{}  \mBbbP{}
3.  base  :  Q[[]]
4.  step  :  \mforall{}[ys:T  List].  (Q[ys]  {}\mRightarrow{}  (\mforall{}y:T.  Q[ys  @  [y]]))
\mvdash{}  base  \mmember{}  Q[[]]


By

---

Latex:
Auto

---

Home Index