apply terminal_eq_of_toList_eq p₁' p₂' h.right
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
u v w : V
e✝ : EdgeBetween G✝ v w
G : Graph V E
v₁ v₂✝ w₁ w₂✝ : V
p₂ : EdgePath G v₂✝ w₂✝
v✝ w✝¹ u✝ : V
e : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
w₂ v₂ w✝ : V
e₂ : EdgeBetween G v₂ w✝
p₂' : EdgePath G w✝ w₂
ih : toList p₁' = toList (cons e₂ p₂') → w✝¹ = v₂ → u✝ = w₂
heq : v✝ = v₂
h : e.edge = e₂.edge ∧ toList p₁' = toList p₂'
⊢ u✝ = w₂
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
u v w : V
e✝ : EdgeBetween G✝ v w
G : Graph V E
v₁ v₂✝ w₁ w₂✝ : V
p₂ : EdgePath G v₂✝ w₂✝
v✝ w✝¹ u✝ : V
e : EdgeBetween G v✝ w✝¹
p₁' : EdgePath G w✝¹ u✝
w₂ v₂ w✝ : V
e₂ : EdgeBetween G v₂ w✝
p₂' : EdgePath G w✝ w₂
ih : toList p₁' = toList (cons e₂ p₂') → w✝¹ = v₂ → u✝ = w₂
heq : v✝ = v₂
h : e.edge = e₂.edge ∧ toList p₁' = toList p₂'
⊢ w✝¹ = w✝