simp [rayToRev, nil_toList]
case nil
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G✝ : Graph V E
x₀✝ : V
G : Graph V E
x₀ τ v✝ : V
hyp : reduced (reverse (nil v✝))
⊢ List.map (fun e => e.nxt.edge) (EdgePath.toList (rayToRev G v✝ v✝ (nil v✝) hyp)) =
    List.map G.bar (List.reverse (EdgePath.toList (nil v✝)))
no goals