Lean/Mathlib: effective inseparability via a self-indexed race at Code.curry c (pair i j)

To prove that a pair is effectively inseparable in Mathlib, with p i j computable and lying outside both W_i and W_j: race (eval (ofNat Code i) x).map (fun _ => 1) against (eval (ofNat Code j) x).map (fun _ => 0) with Partrec.merge'. Take a code c for the race composed with Computable.unpair, and evaluate at e := encode (Code.curry c (Nat.pair i j)). The index is then computable via Code.primrec₂_curry, with no recursion theorem needed. For Smullyan's 'effectively inseparable ⇒ creative', the index of Q ∪ W_k (computable in k) comes the same way: merge' an assert-based enumeration of Q with eval (ofNat Code k), curry over k, and rewrite membership with (hmf (k, x)).2. That .2 is the Dom iff; .2.2 is its mpr. Gotcha: rw [(hmf _).2.2] fails with 'function expected'.