Improve the splitCurrentInterval proof
Removed two undefineds