intro hyp
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
v₁ w₁ v₂ w₂ : V₁
p : Morphism G₁ G₂
inst✝ : CoveringMap p
e₁ : EdgePath G₁ v₁ w₁
e₂ : EdgePath G₁ v₂ w₂
hv : v₁ = v₂
⊢ List.map p.toFuncE (toList e₁) = List.map p.toFuncE (toList e₂) → toList e₁ = toList e₂
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
v₁ w₁ v₂ w₂ : V₁
p : Morphism G₁ G₂
inst✝ : CoveringMap p
e₁ : EdgePath G₁ v₁ w₁
e₂ : EdgePath G₁ v₂ w₂
hv : v₁ = v₂
hyp : List.map p.toFuncE (toList e₁) = List.map p.toFuncE (toList e₂)
⊢ toList e₁ = toList e₂