There was a typo in the Ltac for iSplitL/iSplitR error handling. The MR also adds a test case for this.