perf(verification): shrink and speed up SMT verification conditions

Three improvements to the liquid-type verification path, all
behaviour-preserving on the standard (GIL) build (200+ SMT/typechecking
tests pass):

1. flatten: O(depth^2) -> O(depth) binder alpha-renaming. The eager
   per-binder rename rebuilt the whole remaining constraint at every
   forall, making substitution_in_liquid the hottest function in the
   system. Renamings are now deferred and applied in one pass per
   premise/conclusion. ~2.2x faster flatten on deep constraints;
   verified structurally identical to the old output over 300+ real
   obligations (tests/flatten_rename_test.py).

2. VC simplification before Z3 (smt._simplify_vc): equality elimination
   + relevance slicing. Equality elimination (exact) substitutes x:=Y
   for premises x==Y and drops the binder, collapsing ANF h_i==e_i
   chains. Relevance slicing keeps only premises/functions/variables
   transitively connected to the goal, removing irrelevant `open`-library
   declarations. 3.48x faster validation on deep-constraint programs
   (supermario's 3.5M-char obligation 3.6s -> 1.1s); 0 verdict changes
   over 4,460 obligations across 44 programs. Slicing is always sound;
   see the docstring for the narrow disconnected-inconsistent-premise
   completeness caveat.

3. Thread-local Z3 context (smt._WS) + lock-atomic fresh_counter: makes
   the SMT layer safe for parallel candidate validation under
   free-threaded CPython (python3.14t). The main thread keeps the default
   Z3 context, so external importers and GIL-build behaviour are
   unchanged. Enables ~1.4-2x parallel validation of synthesis
   populations on 3.14t (the parallel driver itself is not yet wired in).

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

Author: alcides

aeon/utils/name.py

@@ -1,3 +1,4 @@
+import threading
 from dataclasses import dataclass, field
 
 from aeon.utils.superscripts import superscript
@@ -8,10 +9,16 @@ class FreshCounter:
 
     def __init__(self):
         self.counter = 0
+        # ``fresh`` runs on worker threads under free-threaded CPython (parallel
+        # SMT validation), where ``self.counter += 1`` is a non-atomic
+        # read-modify-write that can hand out duplicate ids -- which would make
+        # the alpha-renaming in ``flatten`` unsound. Guard with a lock.
+        self._lock = threading.Lock()
 
     def fresh(self) -> int:
-        self.counter += 1
-        return self.counter
+        with self._lock:
+            self.counter += 1
+            return self.counter
 
 
 fresh_counter = FreshCounter()