simp [rayTo, toList_shiftTarget, rayToRev_proj_list,
  reverse_toList, List.map_reverse]
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 p
⊢ List.map (fun e => e.nxt.edge) (EdgePath.toList (rayTo G x₀ τ p hyp)) = EdgePath.toList p
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 p
⊢ List.map (G.bar ∘ G.bar) (EdgePath.toList p) = EdgePath.toList p