---

Step * of Lemma list_extensionality

∀[T:Type]. ∀[a,b:T List].
  (a = b ∈ (T List)) supposing ((∀i:ℕ. (i < ||a|| ⇒ (a[i] = b[i] ∈ T))) and (||a|| = ||b|| ∈ ℤ))
BY
{ (UnivCD THENA Auto') }

1
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)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[a,b:T  List].
    (a  =  b)  supposing  ((\mforall{}i:\mBbbN{}.  (i  <  ||a||  {}\mRightarrow{}  (a[i]  =  b[i])))  and  (||a||  =  ||b||))


By

---

Latex:
(UnivCD  THENA  Auto')

---

Home Index