simp [cons_toList, nil_toList] at h
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✝¹ w v✝ : V
p₂✝ : EdgePath G v✝ v✝
v w✝ : V
e₂ : EdgeBetween G v w✝
p₂ : EdgePath G w✝ v
h : toList (nil v) = toList (cons e₂ p₂)
⊢ nil v = cons e₂ p₂
no goals