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
Edited by Robbert Krebbers