simp [liftTerminal]
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₀ τ
hyp₁ : reduced p₁
hyp₂ : reduced p₂
hyp : [[p₁]] = [[p₂]]
⊢ liftTerminal (proj G x₀) (basepoint G x₀)
      (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) p₁ =
    liftTerminal (proj G x₀) (basepoint G x₀)
      (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) p₂
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₀ τ
hyp₁ : reduced p₁
hyp₂ : reduced p₂
hyp : [[p₁]] = [[p₂]]
⊢ (liftClass (proj G x₀) (basepoint G x₀) ((proj G x₀).toFuncV (basepoint G x₀)) τ
        (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) p₁).τ =
    (liftClass (proj G x₀) (basepoint G x₀) ((proj G x₀).toFuncV (basepoint G x₀)) τ
        (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) p₂).τ