Commit 2026-11-10 15:22 9c5a3cc2

feat: add List.insertIdx_eraseIdx_getElem_perm (#41308) Adds List.insertIdx_eraseIdx_getElem_perm, showing that erasing an element by index and inserting it at any valid position gives a permutation of the original list. This packages the existing lemmas List.perm_insertIdx and List.getElem_cons_eraseIdx_perm into a direct API lemma. AI assistance was used in preparing this PR; I reviewed the statement and proof.