simp [map_toList, reverse_toList, List.map_reverse]
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 : V₁
η : EdgePath G₁ u v
⊢ toList (map (reverse η) f) = toList (reverse (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 : V₁
η : EdgePath G₁ u v
⊢ List.map (f.toFuncE ∘ G₁.bar) (toList η) = List.map (G₂.bar ∘ f.toFuncE) (toList η)