Add `submsetseq` function

This merge requests adds the submsetseq function, which for a list l computes all lists l' such that l' ⊆+ l. It also adds a new lemma about interleave.