Skip to content

upstream some list_numbers lemmas from Perennial

Ralf Jung requested 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