if c':e' = e.bar
  then
    simp [redCons_cons_edge_eq p' c']
    intro p'' red'
    let ⟨u, u', e, p₁, p₂, eqn⟩   := red'.property
    rw [←eqn, ← cons_append] at hyp
    let red := hyp <| cons e' p₁ ++ p₂
    apply red
    apply Reduction.step
  else
    simp [redCons_cons_edge_neq p' c']
    intro p'' red'
    let ⟨u, u', e, p₁, p₂, eqn⟩   := red'.property
    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 e''
      have : e' = e''.bar := by
        ext
        rw [EdgeBetween.bar_eq_bar]
        rw [← leqn.1, leqn.2.1]
      contradiction
    | cons ph pt =>
      symm at eqn
      let tred : ¬ reduced (cons e' p') :=
        tail_reducible_of_split eqn
      contradiction
case refl
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 : V
e' : EdgeBetween G v u
p' : EdgePath G u w
hyp : reduced (cons e' p')
⊢ reduced (redCons e (cons e' p'))
no goals