---

Step * 1 1 of Lemma list_append_singleton_ind

.....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])
BY
{ ((D 0 THENA Auto) THEN NatInd (-1)) }

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

2
.....upcase..... 
1. [T] : Type
2. [Q] : (T List) ⟶ ℙ
3. Q[[]]
4. ∀ys:T List. ∀x:T.  (Q[ys] ⇒ Q[ys @ [x]])
5. n : ℤ
6. [%3] : 0 < n
7. ∀l:T List. ((||l|| = (n - 1) ∈ ℕ) ⇒ Q[l])
⊢ ∀l:T List. ((||l|| = n ∈ ℕ) ⇒ Q[l])

---

Latex:

---

Latex:
.....assertion..... 
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{}n:\mBbbN{}.  \mforall{}l:T  List.    ((||l||  =  n)  {}\mRightarrow{}  Q[l])


By

---

Latex:
((D  0  THENA  Auto)  THEN  NatInd  (-1))

---

Home Index