rw [proj_liftTerminal e₁, proj_liftTerminal e₂]
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ : V
vert : Vert G x₀
e₁ e₂ : EdgePath (univ G x₀) (basepoint G x₀) vert
⊢ liftTerminal (proj G x₀) (basepoint G x₀)
      (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) (EdgePath.map e₁ (proj G x₀)) =
    liftTerminal (proj G x₀) (basepoint G x₀)
      (_ : (proj G x₀).toFuncV (basepoint G x₀) = (proj G x₀).toFuncV (basepoint G x₀)) (EdgePath.map e₂ (proj G x₀))
no goals