apply proj_injective (proj G x₀)
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
⊢ [[e₁]] = [[e₂]]
case a
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
⊢ [[EdgePath.map e₁ (proj G x₀)]] = [[EdgePath.map e₂ (proj G x₀)]]