∀ {l r : List Char} {it : String.Legacy.Iterator},
  String.Legacy.Iterator.ValidFor l r it →
    ∀ n ≤ r.length, String.Legacy.Iterator.ValidFor ((List.take n r).reverse ++ l) (List.drop n r) (it.nextn n)