simp [cons_toList, nil_toList] at h
V : Type u
E : Type v
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
ih : toList p₁' = toList (nil w) → w✝ = w → u✝ = w
h : toList (cons e p₁') = toList (nil w)
heq : v✝ = w
⊢ u✝ = w
no goals