cases prepend_cases e p with
| inl h =>
    rw [h]
| inr h =>
    let ⟨t, h₁, h₂⟩ := h
    rw [h₂, h₁]
    apply Quot.sound
    have split :
      cons e (cons e.bar t) =
        (nil u : EdgePath G u u) ++
          cons e (cons e.bar t) := by
        simp [nil_append]
    rw [split]
    apply Reduction.step
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
⊢ [[cons e p]] = [[redCons e p]]
no goals