have red_cons : reduced (cons e p') := by
  rw [← reverse_reverse (cons e p')]
  apply reverse_reduced
  assumption
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ x₀' u u' : V
e : EdgeBetween G x₀' u
p' : EdgePath G u u'
ih :
  ∀ (hyp : reduced (reverse p')),
    List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' u p' hyp)) =
      List.map G.bar (List.reverse (EdgePath.toList p'))
hyp : reduced (reverse (cons e p'))
⊢ List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' x₀' (cons e p') hyp)) =
    List.map G.bar (List.reverse (EdgePath.toList (cons e p')))
case cons
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ x₀' u u' : V
e : EdgeBetween G x₀' u
p' : EdgePath G u u'
ih :
  ∀ (hyp : reduced (reverse p')),
    List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' u p' hyp)) =
      List.map G.bar (List.reverse (EdgePath.toList p'))
hyp : reduced (reverse (cons e p'))
red_cons : reduced (cons e p')
⊢ List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G u' x₀' (cons e p') hyp)) =
    List.map G.bar (List.reverse (EdgePath.toList (cons e p')))