simp [Setoid.r] at 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₀
h : 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 :
  if h : v₁.τ = v₂.τ then
    Eq.rec (motive := fun a t => v₂.τ = a → HEq (_ : v₁.τ = v₂.τ) t → Prop)
      (fun h_1 =>
        Eq.rec (motive := fun x x_1 =>
          (v₂ : EdgePath G x₀ x) → reduced v₂ → (c : v₁.τ = x) → HEq c (_ : v₁.τ = v₁.τ) → Prop)
          (fun v₂ is_reduced c h => relH H v₁.p v₂) (_ : v₁.τ = v₂.τ) v₂.p (_ : reduced v₂.p) (_ : v₁.τ = v₂.τ))
      (_ : v₁.τ = v₂.τ) (_ : v₂.τ = v₂.τ) (_ : HEq (_ : v₁.τ = v₂.τ) (_ : v₁.τ = v₂.τ))
  else False
⊢ v₁.τ = v₂.τ