@[simp]

theorem Std.Iter.joinString_eq {α β : Type} [Iterator α Id β] [Iterators.Finite α Id] [ToString β] {it : Iter β} : it.joinString = String.join (List.map toString it.toList)

@[simp]

theorem Std.Iter.intercalateString_eq {α β : Type} [Iterator α Id β] [Iterators.Finite α Id] [ToString β] {s : String.Slice} {it : Iter β} : intercalateString s it = s.copy.intercalate (List.map toString it.toList)