match p₁ with
    | nil _ =>
      rw [nil_append] at eqn
      let leqn := congrArg EdgePath.toList eqn
      simp [cons_toList, nil_toList, append_toList] at leqn
      rename_i u'' e''
      apply c
      rw [← e.init_eq, ← e'.term_eq, ← G.ι_bar, ← leqn.2.1, bar_bar]
    | cons ph pt =>
      symm at eqn
      let tred : ¬ reduced (cons e' p') :=
        tail_reducible_of_split eqn
      contradiction
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
u✝ v w' : V
e✝ : EdgeBetween G u✝ v
p : EdgePath G v w'
w w'' : V
e' : EdgeBetween G v w''
p' : EdgePath G w'' w
hyp : reduced (cons e' p')
c : ¬w'' = u✝
p'' : EdgePath G u✝ w
red' : Reduction (cons e✝ (cons e' p')) p''
u u' : V
e : EdgeBetween G u u'
p₁ : EdgePath G u✝ u
p₂ : EdgePath G u w
eqn : p₁ ++ cons e (cons (EdgeBetween.bar e) p₂) = cons e✝ (cons e' p')
⊢ False
no goals