split up list.v into smaller files

This generally follows the organization we decided for here. However, I had to move the proof of dependability of submseteq and Permutation into list_misc since it needs the monadic operations -- and I did not want list_relations to import list_monad; the relations "feel" more fundamental than the monadic operations, and that is also the order in which they appeared in the old file. I moved NoDup into list_relations.

I am not sure how to best review this -- the diff will be basically useless. I have produced a diff of "the concatenation of all the new files" with the old file; maybe that is helpful. You can find it at https://gitlab.mpi-sws.org/-/snippets/1708. Note that I concatenated the files in the order "basics, misc, relations, monad, tactics" -- that is not the dependency order in the new system, but it is the closest to their original order, so this minimizes the diff. I can produce the diff with the new files in dependency order instead if you prefer that.