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