---

Step * 1 of Lemma map_functionality


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')
BY
{ ((RewriteWith [7] [] 0 THENA Auto) THEN BLemma `map_permr_func` THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  f  :  A  {}\mrightarrow{}  B
4.  f'  :  A  {}\mrightarrow{}  B
5.  as  :  A  List
6.  as'  :  A  List
7.  f  =  f'
8.  as  \mequiv{}(A)  as'
\mvdash{}  map(f;as)  \mequiv{}(B)  map(f';as')


By

---

Latex:
((RewriteWith  [7]  []  0  THENA  Auto)  THEN  BLemma  `map\_permr\_func`  THEN  Auto)

---

Home Index