Make adequacy apply to multiple initial threads
This MR adapts wp_strong_adequacy
to apply to an initial configuration with multiple threads. This is necessary for RefinedC since it currently does not have a fork operation, but instead relies on multiple threads in the initial configuration for concurrency.
This MR is WIP because I don't know how to prove big_sepL2_fupd
without the proof mode. @robbertkrebbers how would you prove it?