---

Step * 1 1 2 of Lemma list_append_singleton_ind

.....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])
BY
{ Auto' }

1
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])
8. l : T List
9. ||l|| = n ∈ ℕ
⊢ Q[l]

---

Latex:

---

Latex:
.....upcase..... 
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.  n  :  \mBbbZ{}
6.  [\%3]  :  0  <  n
7.  \mforall{}l:T  List.  ((||l||  =  (n  -  1))  {}\mRightarrow{}  Q[l])
\mvdash{}  \mforall{}l:T  List.  ((||l||  =  n)  {}\mRightarrow{}  Q[l])


By

---

Latex:
Auto'

---

Home Index