no goals
α : Type u_1
f : Char → α → α
init : α
x✝ : Substring
h✝ : Valid x✝
w✝² w✝¹ w✝ : List Char
h : ValidFor w✝² w✝¹ w✝ x✝
⊢ Substring.foldr f init x✝ = List.foldr f init (toString x✝).data
simp [h.foldr, h.toString]