Also rename seq_S_end_app to seq_S_snoc, which I think better matches our usual name for lemmas involving _ ++ [_].
seq_S_end_app
seq_S_snoc
_ ++ [_]
The proofs are by @tchajed.