The lemma seq_S is present in Coq's stdlib since Coq 8.12, and is the same as our lemma seq_S_snoc.
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.