simp [Setoid.r, relH]
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
τ : V
p₁ p₂ : EdgePath G x₀ τ
red₁ : reduced p₁
red₂ : reduced p₂
⊢ Setoid.r { τ := τ, p := p₁, is_reduced := red₁ } { τ := τ, p := p₂, is_reduced := red₂ } ↔ [[p₁ ++ reverse p₂]] ∈ H
no goals