---

Step * 1 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]])
⊢ ∀zs:T List. Q[zs]
BY
{ Assert ∀n:ℕ. ∀l:T List.  ((||l|| = n ∈ ℕ) ⇒ Q[l]) }

1
.....assertion..... 
1. [T] : Type
2. [Q] : (T List) ⟶ ℙ
3. Q[[]]
4. ∀ys:T List. ∀x:T.  (Q[ys] ⇒ Q[ys @ [x]])
⊢ ∀n:ℕ. ∀l:T List.  ((||l|| = n ∈ ℕ) ⇒ Q[l])

2
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]

---

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]])
\mvdash{}  \mforall{}zs:T  List.  Q[zs]


By

---

Latex:
Assert  \mforall{}n:\mBbbN{}.  \mforall{}l:T  List.    ((||l||  =  n)  {}\mRightarrow{}  Q[l])

---

Home Index