if c:w'' = u then
  cases c
  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
else
  simp [redCons_cons_vertex_neq e e' 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 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')
⊢ reduced (redCons e (cons e' p'))
no goals