---

Step * 1 of Lemma map_equal


1. T : Type
2. T' : Type
3. a : T List
4. f : T ⟶ T'
5. g : T ⟶ T'
6. ∀i:ℕ. (i < ||a|| ⇒ ((f a[i]) = (g a[i]) ∈ T'))
⊢ map(f;a) = map(g;a) ∈ (T' List)
BY
{ (BackThruLemma `list_extensionality` THENA Auto) }

1
1. T : Type
2. T' : Type
3. a : T List
4. f : T ⟶ T'
5. g : T ⟶ T'
6. ∀i:ℕ. (i < ||a|| ⇒ ((f a[i]) = (g a[i]) ∈ T'))
⊢ ||map(f;a)|| = ||map(g;a)|| ∈ ℤ

2
1. T : Type
2. T' : Type
3. a : T List
4. f : T ⟶ T'
5. g : T ⟶ T'
6. ∀i:ℕ. (i < ||a|| ⇒ ((f a[i]) = (g a[i]) ∈ T'))
⊢ ∀i:ℕ. (i < ||map(f;a)|| ⇒ (map(f;a)[i] = map(g;a)[i] ∈ T'))

---

Latex:

---

Latex:

1.  T  :  Type
2.  T'  :  Type
3.  a  :  T  List
4.  f  :  T  {}\mrightarrow{}  T'
5.  g  :  T  {}\mrightarrow{}  T'
6.  \mforall{}i:\mBbbN{}.  (i  <  ||a||  {}\mRightarrow{}  ((f  a[i])  =  (g  a[i])))
\mvdash{}  map(f;a)  =  map(g;a)


By

---

Latex:
(BackThruLemma  `list\_extensionality`  THENA  Auto)

---

Home Index