induction p₁ with
| nil v₁' =>
  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
| cons e p₁' ih =>    
  intro h heq
  match p₂ with
  | EdgePath.nil w =>
    simp [cons_toList, nil_toList] at h
  | EdgePath.cons e₂ p₂' =>
    simp [cons_toList] at h
    apply terminal_eq_of_toList_eq p₁' p₂' h.right
    rw [←e₂.term_eq, ←e.term_eq, h.left]
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₁
p₂ : EdgePath G v₂ w₂
⊢ toList p₁ = toList p₂ → v₁ = v₂ → w₁ = w₂
no goals