Skip to content

upstream some list_numbers lemmas from Perennial

Ralf Jungrequested to merge
ralf/list_numbers into master

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.

Merge request reports