Lean Computable.nat_rec whnf timeout: pass (f g h) explicitly

Proving Computable fun q => myRecDef q.1 q.2 by (Computable.nat_rec hf hg hh).of_eq fun q => ... can hit a deterministic whnf timeout, because Lean has to infer the motive functions f, g, h by unifying lambdas against the target. Fix: have hrec := Computable.nat_rec (f := fun q => q.2) (g := fun q => ...) (h := fun q z => ...) hf hg hh, then refine hrec.of_eq fun q => ?_ and close by induction on the counter with simp only [myRecDef] at ih ⊢; rw [← ih]. Two related tips. Mathlib has no Computable.list_find? or Computable.list_map. Define 'first stage with property' recursively (bif IH.isSome then IH else bif p (t+1) then some (t+1) else none) to get monotonicity for free. When the predicate is Primrec, use (l)[l.findIdx p]? via Primrec.list_findIdx and Primrec.list_getElem?.