theorem List.drop_eraseIdx {α : Type u_1} (l : List α) (i j : ℕ) : (drop i l).eraseIdx j = drop i (l.eraseIdx (i + j))

theorem List.reverse_eraseIdx {α : Type u_1} {l : List α} {i : ℕ} (hi : i < l.length) : l.reverse.eraseIdx i = (l.eraseIdx (l.length - i - 1)).reverse

theorem List.finite_sublist {α : Type u_1} (l : List α) : {l' : List α | l'.Sublist l}.Finite