intro 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₀ τ
hyp₁ : reduced p₁
hyp₂ : reduced p₂
⊢ [[p₁]] = [[p₂]] → p₁ = 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₂]]
⊢ p₁ = p₂