rw [h]
case refl.refl
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
τ₀ τ₁ : V
e : EdgeBetween G τ₀ τ₁
p : EdgePath G x₀ τ₀
is_reduced✝¹ : reduced p
p' : EdgePath G x₀ τ₀
is_reduced✝ : reduced p'
e' : EdgeBetween G τ₀ τ₁
c : τ₀ = τ₀ ∧ τ₁ = τ₁
a✝ : [[p ++ reverse p']] ∈ H
h : e = e'
⊢ e.edge = e'.edge
no goals