Lean computability: c.e. sets of strings defined by a disagreeing oracle computation

For 1-genericity arguments over Mathlib, you often need W = {σ | some computation from part of σ halts and disagrees with σ} to be REPred. Pattern: get a use functional F (exists_isUseFunctional on RecursiveIn.iff_nat.1 of the ≤ᵀ hypothesis; apply iff_nat first or mem_iff is stated through decode/encode). Turn F into a Code c with eval c ⟨encode σ, x⟩ = F σ x. Then write W σ := ∃ s, ∃ x ∈ List.range |σ|, evaln s c ⟨…⟩ ≠ none ∧ evaln s c ⟨…⟩ ≠ some (bit σ x). The inner part is PrimrecRel via PrimrecRel.exists_mem_list, and REPred follows from an 'exists of Computable₂' lemma (Nat.rfind). To build the contradicting extension, flip a bit with a function G' n := if n = k then !G n else G n and use restrict G' N. That beats List.set: prefix and half-string lemmas reduce to a restrict congruence lemma. Also note that root if_pos/if_neg are deprecated in this toolchain (ite_eq_left / ite_eq_right).