Fix: enable bool(x) == y equality resolution

[keyboardDrummer-bot]

Summary

Fixes #945 — the analyzer could not resolve bool(x) == y equality assertions because Python's bool() builtin was not mapped to any Laurel function.

Changes

1. PythonRuntimeLaurelPart.lean

• Added float to Any_to_bool — the precondition and body were missing the float branch, so Any_to_bool couldn't handle float inputs. This also partially addresses Soundness bug: PNot returns exception for None and DictStrAny inputs instead of computing not #934.
• Added to_bool_any function — a wrapper that returns from_bool(Any_to_bool(v)), converting the bool result back to Any so it can be compared with other Any values like from_bool(true).

2. PythonToLaurel.lean

• Added \"bool\" => \"to_bool_any\" to reMapFunctionName — previously, bool() calls had no name mapping, so hasModel returned false and the call was translated to Hole. Now it maps to the new to_bool_any function.

Why this fixes the issue

When Python code like assert bool(None) == False is analyzed:

1. bool(None) is now translated to to_bool_any(from_None()) instead of Hole
2. to_bool_any calls Any_to_bool which returns false for None, then wraps it as from_bool(false)
3. The equality from_bool(false) == from_bool(false) is trivially resolved by the SMT solver

Verification

Full lake build passes (508 jobs). All existing test modules build successfully:

• VerifyPythonTest ✅
• ToLaurelTest ✅
• PreludeVerifyTest ✅