[Suggestion] Rewrite rule: `List.any` with equality lambda to `List.elem`

`List.any l (fun x => x == k)` is currently passed as-is to Z3, which struggles to reason about bound variables in lambda expressions and runs indefinitely on theorems involving this pattern.

A rewrite rule transforming this into `List.elem k l` before SMT translation would eliminate the bound variable. As a side effect, some theorems involving this pattern become provable in the optimization phase alone, without requiring Z3 at all.