apply eq_of_toList_eq
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_4
E₂ : Type u_3
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
u v w : V₁
η : EdgePath G₁ u v
η' : EdgePath G₁ v w
⊢ map (η ++ η') f = map η f ++ map η' f
case a
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_4
E₂ : Type u_3
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
u v w : V₁
η : EdgePath G₁ u v
η' : EdgePath G₁ v w
⊢ toList (map (η ++ η') f) = toList (map η f ++ map η' f)