Merged requested to merge ci/robbert/seq_S into master
seq_S is present in Coq's stdlib since Coq 8.12, and is the same as our lemma
MR !211 (merged) accidentally used the lemma
seq_S from the stdlib, and hence CI failed with Coq 8.10 and Coq 8.11.
This MR adds a copy of the lemma from the stdlib, which we can remove once we drop support for Coq 8.10 and Coq 8.11.