simp [relH]
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
τ : V
v₁ v₂ v₃ : EdgePath G x₀ τ
⊢ relH H v₁ v₂ → relH H v₂ v₃ → relH H v₁ v₃
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
τ : V
v₁ v₂ v₃ : EdgePath G x₀ τ
⊢ [[v₁ ++ reverse v₂]] ∈ H → [[v₂ ++ reverse v₃]] ∈ H → [[v₁ ++ reverse v₃]] ∈ H