simp [map_toList]
V : Type u
E : Type v
V₁ : Type ?u.140325
E₁ : Type ?u.140324
V₂ : Type ?u.140329
E₂ : Type ?u.140328
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
p : Morphism G₁ G₂
inst✝ : CoveringMap p
v₁ w₁ : V₁
e : EdgePath G₁ v₁ w₁
⊢ List.map p.toFuncE (toList e) = toList (EdgePath.map e p)
no goals