intro h₁ 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.τ₀ →
    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.τ₀
h₂ : e.τ₁ = τ₁
⊢ ∃ nxt p', ∃ (red : reduced p'), e = { τ₀ := τ₀, τ₁ := τ₁, nxt := nxt, p := p', is_reduced := red }