induction p with
| nil _ =>
  simp [reduction_nil]
| cons e p ih =>
  rw [reduction_cons]
  have teq : reduction p = p := by
    apply ih
    apply tail_reduced
    assumption
  rw [teq]
  apply redCons_eq_cons_of_reduced
  assumption
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
v w : V
p : EdgePath G v w
hyp : reduced p
⊢ reduction p = p
no goals