cases p₁ with
| nil _ =>
  rw [nil_append] at eqn
  let leqn := congrArg EdgePath.toList eqn
  simp [cons_toList, nil_toList] at leqn
| cons h t =>
  rw [cons_append] at eqn
  let leqn := congrArg EdgePath.toList eqn
  simp [cons_toList, nil_toList, append_toList] at leqn
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u✝ v : V
e✝ : EdgeBetween G u✝ v
p' : EdgePath G u✝ v
red' : Reduction (cons e✝ (nil v)) p'
u u' : V
e : EdgeBetween G u u'
p₁ : EdgePath G u✝ u
p₂ : EdgePath G u v
eqn : p₁ ++ cons e (cons (EdgeBetween.bar e) p₂) = cons e✝ (nil v)
⊢ False
no goals