---

Step * of Lemma list_append_ind

∀[T:Type]. ∀[Q:(T List) ⟶ ℙ].
  (Q[[]] ⇒ (∀x:T. Q[[x]]) ⇒ (∀ys,ys':T List.  (Q[ys] ⇒ Q[ys'] ⇒ Q[ys @ ys'])) ⇒ {∀zs:T List. Q[zs]})
BY
{ (Unfold `guard` 0 THEN InductionOnList THEN Auto) }

1
1. [T] : Type
2. [Q] : (T List) ⟶ ℙ
3. Q[[]]@i
4. ∀x:T. Q[[x]]@i
5. ∀ys,ys':T List.  (Q[ys] ⇒ Q[ys'] ⇒ Q[ys @ ys'])@i
6. u : T@i
7. v : T List@i
8. Q[v]@i
⊢ Q[[u / v]]

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[Q:(T  List)  {}\mrightarrow{}  \mBbbP{}].
    (Q[[]]
    {}\mRightarrow{}  (\mforall{}x:T.  Q[[x]])
    {}\mRightarrow{}  (\mforall{}ys,ys':T  List.    (Q[ys]  {}\mRightarrow{}  Q[ys']  {}\mRightarrow{}  Q[ys  @  ys']))
    {}\mRightarrow{}  \{\mforall{}zs:T  List.  Q[zs]\})


By

---

Latex:
(Unfold  `guard`  0  THEN  InductionOnList  THEN  Auto)

---

Home Index