#245 (closed) talks about IntoAnd, but I mirrored what we got for big_sepL and that's IntoSep.
However, I also remembered why we didn't do that for lambdaRust: there, array-mapsto is fractional, and then there is the question whether one wants to split at the fraction or the list. We decided that the proofmode would split at the fraction. If we agree that's the more reasonable choice, we should not add the splitting-at-the-list now because then we couldn't extend array-mapsto to fractions later.