{m : Type → Type u_1} →
  (motive : Std.IterM m UInt8 → Sort u_2) →
    (x : Std.IterM m UInt8) →
      ((s : String.Slice) → (offset : String.Pos.Raw) → motive { internalState := { s := s, offset := offset } }) →
        motive x