---

Step * of Lemma map_permr_func

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

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

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index