match p with
| nil _ =>
  simp [redCons_nil]
  apply reduced_singleton
| cons e' p' =>
  rename_i w' w''
  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
hyp : reduced p
⊢ reduced (redCons e p)
no goals