try to simplify a proof

[OwenConoly]

I spent a while looking at the proof of withInterference_parallel (in the ModelChecking file) without being able to understand it, so I tried to write a simpler proof.

Obviously my style of writing proof scripts is a bit incongruous with the rest of the file, but I think a proof along these lines could be easier to understand.