Commit 2025-11-29 21:29 874226a3

feat(Data/List/Cycle): generalize next theorems from x ∈ l ∧ x ≠ l.getLast to x ∈ l.dropLast (#31958) This is a generalization since x ∈ l ∧ x ≠ l.getLast → x ∈ l.dropLast is true for all x, l, but the reverse direction is false: consider x = 2, l = [1, 2, 3, 4, 2]. Since List.next looks for the first occurrence of x, the theorems stay true after this generalization.