match p₂ with
| EdgePath.nil v => 
  intro h heq
  rw [nil_toList] at h      
  exact heq
| EdgePath.cons e₂ p₂  =>
  intro h
  simp [cons_toList, nil_toList] at h
case nil
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₁' : V
⊢ toList (nil v₁') = toList p₂ → v₁' = v₂ → v₁' = w₂
no goals