match p, p', e, e', eq₂ with
| p, p', e, e', rfl => 
  simp [cons_toList,  eq₃]
  ext
  symm
  assumption
V : Type u
E : Type v
G✝ : Graph V E
u✝ v✝ w✝ : V
e✝ : EdgeBetween G✝ v✝ w✝
G : Graph V E
v w w' u : V
e : EdgeBetween G v w
e' : EdgeBetween G v w'
p : EdgePath G w u
p' : EdgePath G w' u
eq₁ : e.edge = e'.edge
eq₂ : w = w'
eq₃ : p = (_ : w' = w) ▸ p'
⊢ cons e' p' = cons e p
no goals