Separating big operator over two lists.

After having needed this multiple times already, and having defined this construction in an ad-hoc manner, I decided to do it properly.

Notes:

• I decided to define it in a computation way (i.e. by recursion over both lists) to get nice behavior with simpl.
• I copied all lemmas from big_sepL but removed those that I couldn't generalize in a sensible way. There are probably many more results that could be useful, but those could be added later.

Main point to rant about: do we like the notation [∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2