Commit 2024-08-16 23:11 45d8a0f5

chore: clean up List/Indexes (#15825) There had been a bit of a mess here of shims connecting back to a Lean 3 era definition. Rip it all out, replacing the proofs that required these shims, and deprecate the now unneeded mess.