Commit 2022-08-24 05:21 757e73c5

feat(data/seq/seq): prove seq.ext earlier (#15830) We heavily golf seq.ext and move it to almost the beginning of the file. Doing this breaks the proof of seq.of_list_cons, which we also change and golf by adding a few trivial simp lemmas (not all of them are needed, but might as well add them).