have eq_edgepath : p₁.path.toList = p₂.path.toList := by
  apply lifts_homotopic p p₁.path p₂.path rfl
  apply eq_edgepath_aux
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₂
p : Morphism G₁ G₂
inst✝ : CoveringMap p
v₁ : V₁
v₂ w₂ : V₂
h₁ h₂ : p.toFuncV v₁ = v₂
e : EdgePath G₂ v₂ w₂
p₁ : PathLift p v₁ h₁ e
p₂ : PathLift p v₁ h₂ e
eq_edgepath_aux : List.map p.toFuncE (toList p₁.path) = List.map p.toFuncE (toList p₂.path)
⊢ p₁ = p₂
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₂
p : Morphism G₁ G₂
inst✝ : CoveringMap p
v₁ : V₁
v₂ w₂ : V₂
h₁ h₂ : p.toFuncV v₁ = v₂
e : EdgePath G₂ v₂ w₂
p₁ : PathLift p v₁ h₁ e
p₂ : PathLift p v₁ h₂ e
eq_edgepath_aux : List.map p.toFuncE (toList p₁.path) = List.map p.toFuncE (toList p₂.path)
eq_edgepath : toList p₁.path = toList p₂.path
⊢ p₁ = p₂