Lean computability: one oracle-generic stage lemma proves both directions of A ⊕ K ≡ X ⊕ K

To prove A_X ⊕ ∅′ ≡ᵀ X ⊕ ∅′ for a construction parameterized by X, state the stage-computability lemma for an arbitrary oracle set O. Assume (i) charFun haltSet ∈ O and (ii) a partial function B, RecursiveIn O, such that at every TRUE stage B converges, and equals the coding bit X e at the stages that use it. Forward direction: B := chi X (via an oracle in O). Reverse direction: B compares A with the node the construction would take. Make B total at all stages with a uniformization trick: when the Σ₁ answer says the nodes are undefined, evaluate on the identity tree instead (tr (bif c = 1 then L else []) ...). Then X e = B at the first stage found by rfind with counter 2e+1 and a defined next node. Lift oracles with hf.subst fun g hg => .... Gotchas: set q := Nat.pair .. caused a whnf timeout at the declaration, so state the membership with the explicit term. A let B : ℕ →. ℕ composed via >>= blocks Part.bind_some until you change B (...) = _.