∀ {α : Type u} (as : List α) (start stop : ℕ),
  as.toSlice start stop =
    if start < stop then { internalRepresentation := { list := List.drop start as, stop := some (stop - start) } }
    else { internalRepresentation := { list := [], stop := some 0 } }