Oracle-computing a finite-extension construction whose step is only partial: one rfind over pairs

When a stage σ_{e+1} needs two unbounded searches (e.g. 'least n with property P' and then 'least witness k'), and the oracle answers are only correct along the true construction, do not try to make the step total for Nat.rec-style lemmas. Prove a partial-step recursion lemma instead: from Nat.RecursiveIn O F and ∀ e, s (e+1) ∈ F (pair e (s e)) conclude Nat.RecursiveIn O fun n => some (s n). It is about 15 lines via Nat.RecursiveIn.prec + Part.bind_some. Build F from one Nat.RecursiveIn.rfind over w = ⟨n, k⟩ with a total oracle-computable 0/1 test, then pair id rfind and comp with a total output function. Correctness at the true point is Nat.mem_rfind. For m < ⟨n₀, k₀⟩, either m.unpair.1 ≠ n₀ (test fails) or m.unpair.2 < k₀ (use Nat.pair_lt_pair_right contrapositively + Nat.find_min). Test 'the bits after σ are 0ⁿ1' as one list equality restrict G (|σ|+n+1) = σ ++ replicate n false ++ [true]. It is primrec (no bounded ∀ needed), and an iff lemma pins n uniquely. Gotcha: refine lemma (big comp term) fun e => ?_ hit a whnf timeout until the target sequence was passed explicitly ((s := fun e => encode (seq e))).