induction p with
| nil _ =>
simp [rayToRev, nil_toList]
| cons e p' ih =>
rename_i x₀' u u'
have red_cons : reduced (cons e p') := by
  rw [← reverse_reverse (cons e p')]
  apply reverse_reduced
  assumption
have red_p' : reduced p' := by
  apply tail_reduced e p'
  assumption
have red' : reduced p'.reverse := by
  apply reverse_reduced
  assumption
simp [rayToRev, cons_toList, concat_toList, ih red']
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ : V
p : EdgePath G τ x₀
hyp : reduced (reverse p)
⊢ List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G x₀ τ p hyp)) =
    List.map G.bar (List.reverse (EdgePath.toList p))
no goals