---

Step * 1 of Lemma list_extensionality


1. T : Type
2. a : T List
3. b : T List
4. ||a|| = ||b|| ∈ ℤ
5. ∀i:ℕ. (i < ||a|| ⇒ (a[i] = b[i] ∈ T))
⊢ a = b ∈ (T List)
BY
{ (((((MoveToConcl 3 THEN ListInd 2) THEN (D 0 THENA Auto)) THEN ListInd (-1)) THEN Reduce 0) THEN Auto') }

1
1. T : Type
2. u : T@i
3. v : T List@i
4. ∀b:T List. ((||v|| = ||b|| ∈ ℤ) ⇒ (∀i:ℕ. (i < ||v|| ⇒ (v[i] = b[i] ∈ T))) ⇒ (v = b ∈ (T List)))
5. u1 : T@i
6. v1 : T List@i
7. (||[u / v]|| = ||v1|| ∈ ℤ) ⇒ (∀i:ℕ. (i < ||[u / v]|| ⇒ ([u / v][i] = v1[i] ∈ T))) ⇒ ([u / v] = v1 ∈ (T List))
8. (||v|| + 1) = (||v1|| + 1) ∈ ℤ
9. ∀i:ℕ. (i < ||v|| + 1 ⇒ ([u / v][i] = [u1 / v1][i] ∈ T))
⊢ [u / v] = [u1 / v1] ∈ (T List)

---

Latex:

---

Latex:

1.  T  :  Type
2.  a  :  T  List
3.  b  :  T  List
4.  ||a||  =  ||b||
5.  \mforall{}i:\mBbbN{}.  (i  <  ||a||  {}\mRightarrow{}  (a[i]  =  b[i]))
\mvdash{}  a  =  b


By

---

Latex:
(((((MoveToConcl  3  THEN  ListInd  2)  THEN  (D  0  THENA  Auto))  THEN  ListInd  (-1))  THEN  Reduce  0)
  THEN  Auto'
  )

---

Home Index