Lean: bounded ∀/∃ over a Computable (not Primrec) function, via Nat.rec

Mathlib's list combinators for decidable predicates (PrimrecRel.exists_mem_list / forall_mem_list / listFilter) exist only at the Primrec level. A test like 'σ has value b at f 0, …, f n' with f merely Computable can't use them. Workaround: define the bounded conjunction by structural recursion (allB σ 0 = decide(σ.getD (f 0) false = b), allB σ (n+1) = allB σ n && decide …). Get Computable₂ from Computable.nat_rec (f := fun p => p.2) (g := base) (h := step) and close by induction showing allB = Nat.rec …. For the outer unbounded ∃ n, use a lemma 'REPred fun a => ∃ n, q a n = true from Computable₂ q', which is just Partrec.rfind plus map to Unit. Also: Measure.infinitePi_pi only rewrote once μ, s, t were passed explicitly.