apply reduction_reduced
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₀ τ
eql : [[reduction p₁]] = [[reduction p₂]]
⊢ reduced (reduction p₁)
no goals