∀ (s : String) (p : Char → Bool) (b i : String.Pos.Raw) (r : List String),
  s.splitAux p b i r =
    if h : String.Pos.Raw.atEnd s i = true then
      have r := String.Pos.Raw.extract s b i :: r;
      r.reverse
    else
      have this := ⋯;
      if p (String.Pos.Raw.get s i) = true then
        have i' := String.Pos.Raw.next s i;
        s.splitAux p i' i' (String.Pos.Raw.extract s b i :: r)
      else s.splitAux p b (String.Pos.Raw.next s i) r