---

Step * 1 2 of Lemma list_append_singleton_ind


1. [T] : Type
2. [Q] : (T List) ⟶ ℙ
3. Q[[]]
4. ∀ys:T List. ∀x:T.  (Q[ys] ⇒ Q[ys @ [x]])
5. ∀n:ℕ. ∀l:T List.  ((||l|| = n ∈ ℕ) ⇒ Q[l])
⊢ ∀zs:T List. Q[zs]
BY
{ TACTIC:(Auto THEN InstHyp [||zs||; zs] 5⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [Q]  :  (T  List)  {}\mrightarrow{}  \mBbbP{}
3.  Q[[]]
4.  \mforall{}ys:T  List.  \mforall{}x:T.    (Q[ys]  {}\mRightarrow{}  Q[ys  @  [x]])
5.  \mforall{}n:\mBbbN{}.  \mforall{}l:T  List.    ((||l||  =  n)  {}\mRightarrow{}  Q[l])
\mvdash{}  \mforall{}zs:T  List.  Q[zs]


By

---

Latex:
TACTIC:(Auto  THEN  InstHyp  [||zs||;  zs]  5\mcdot{}  THEN  Auto)

---

Home Index