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