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]
case cons
V : Type u
E : Type v
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✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p₁' : EdgePath G w✝ u✝
ih : toList p₁' = toList p₂ → w✝ = v₂ → u✝ = w₂
h : toList (cons e p₁') = toList p₂
heq : v✝ = v₂
⊢ u✝ = w₂
no goals