intro h
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
e : Edge G x₀
τ₀ : V
⊢ τ₀ = e.τ₀ → ∃ τ₁ nxt p', ∃ (red : reduced p'), e = { τ₀ := τ₀, τ₁ := τ₁, nxt := nxt, p := p', is_reduced := red }
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
e : Edge G x₀
τ₀ : V
h : τ₀ = e.τ₀
⊢ ∃ τ₁ nxt p', ∃ (red : reduced p'), e = { τ₀ := τ₀, τ₁ := τ₁, nxt := nxt, p := p', is_reduced := red }