Add `seq_set_pred_disjoint`

A sort of "dual" to seq_set_S_disjoint.

Thanks for the MR.

The names of these lemmas, including those that were already there, make little sense.

I wondered why the original one was called seq_set_S_disjoint, and I noticed that's because it is related to seq_set_S_union: seq_set_S_disjoint says that the RHS of seq_set_S_union is disjoint.

Could you make sure that at least seq_set_S_union and seq_set_S_disjoint remain together. Apart from that, I don't have suggestions for better names, so if you don't have any ideas either I'm happy to merge this once the order is restored.

added 1 commit

• d4b57ae8 - Add `seq_set_start_disjoint`

Compare with previous version

Hi Robbert.

I did a forced update, and moved the lemma up. I've also changed the name to seq_set_start_disjoint, not sure if it is a better name though.

Any update on this, @robbertkrebbers?

LGTM! Sorry for forgetting to come back to this.

@jung any idea why there is a failed CI pipeline here. As such, I cannot merge via the Gitlab webinterface.

mentioned in commit 0d9f04c5

merged

I was able to merge with the webinterface. Just ignore the fact that the button is red, and click it :)

The failed pipeline is due to CI not working in forks. Forks don't have access to our CI runners.

mentioned in merge request !144 (merged)