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.