apply l nxt.term_eq
case e_8
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
τ : V
p : EdgePath G x₀ τ
is_reduced : reduced p
τ₀ τ₁ : V
nxt : EdgeBetween G τ₀ τ₁
p' : EdgePath G x₀ τ₀
is_reduced' : reduced p'
h : τ = G.ι nxt.edge
l : ∀ {τ : V} (pf : Graph.τ G nxt.edge = τ), HEq (_ : Graph.τ G nxt.edge = Graph.τ G nxt.edge) pf
⊢ HEq (_ : Graph.τ G nxt.edge = Graph.τ G nxt.edge) (_ : Graph.τ G nxt.edge = τ₁)
no goals