---

Step * of Lemma map_functionality

∀A,B:Type. ∀f,f':A ⟶ B. ∀as,as':A List.  ((f = f' ∈ (A ⟶ B)) ⇒ (as ≡(A) as') ⇒ (map(f;as) ≡(B) map(f';as')))
BY
{ Auto }

1
1. A : Type
2. B : Type
3. f : A ⟶ B
4. f' : A ⟶ B
5. as : A List
6. as' : A List
7. f = f' ∈ (A ⟶ B)
8. as ≡(A) as'
⊢ map(f;as) ≡(B) map(f';as')

---

Latex:

---

Latex:
\mforall{}A,B:Type.  \mforall{}f,f':A  {}\mrightarrow{}  B.  \mforall{}as,as':A  List.
    ((f  =  f')  {}\mRightarrow{}  (as  \mequiv{}(A)  as')  {}\mRightarrow{}  (map(f;as)  \mequiv{}(B)  map(f';as')))


By

---

Latex:
Auto

---

Home Index