exact hyp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p₁ p₂ : EdgePath G x₀ τ
red₁ : [[reduction p₁]] = [[p₁]]
red₂ : [[reduction p₂]] = [[p₂]]
l₁ : liftTerminal (proj G x₀) (basepoint G x₀)
    (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) (reduction p₁) =
  liftTerminal (proj G x₀) (basepoint G x₀)
    (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) p₁ :=
  liftTerminal_eq_of_homotopic (proj G x₀) (basepoint G x₀) rfl red₁
_l₂ : liftTerminal (proj G x₀) (basepoint G x₀)
    (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) (reduction p₂) =
  liftTerminal (proj G x₀) (basepoint G x₀)
    (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) p₂ :=
  liftTerminal_eq_of_homotopic (proj G x₀) (basepoint G x₀) rfl red₂
hyp : reduction p₁ = reduction p₂
⊢ reduction p₁ = reduction p₂
no goals