Added `bigcat` over sequences

Previously, we only had bigcat over over ranges. I added

• a new notation for concatenating over a sequence
• A bunch of useful lemmas that I needed for CERTA.

The code still needs to be properly commented, I will do that soon.

changed the description

resolved all threads

resolved all threads

added 2 commits

• 35b1f932 - Polish
• 64b15bbc - More polish, comments

Compare with previous version

This is now ready for another iteration!