intro h
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
v₁ v₂ : Vert G x₀
⊢ Setoid.r v₁ v₂ → 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₂ : Vert G x₀
h : Setoid.r v₁ v₂
⊢ v₁.τ = v₂.τ