simp [c]
case pos
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₀
c : v₁.τ = v₂.τ
h :
  Eq.rec (motive := fun a t => v₂.τ = a → HEq (_ : v₁.τ = v₂.τ) t → Prop)
    (fun h =>
      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₂.τ))
⊢ v₁.τ = v₂.τ
no goals