Lean: whnf timeout from Computable₂.partrec₂ (f := ...) on a PrimrecPred.decide

Writing Computable₂.partrec₂ (f := fun n t => decide (P n t)) (hp.decide.to_comp) (or (show Computable₂ ... from ...).partrec₂) hung with '(deterministic) timeout at whnf', reported at the theorem's first line, so it looked like the whole proof was slow. Fix: elaborate in steps. have h1 : Primrec fun q : ℕ × ℕ => decide (P q.1 q.2) := hp.decide, then have h2 : Computable (fun q => ...) := h1.to_comp, then exact h2.partrec. Here the goal Partrec₂ (fun n t => Part.some ...) is defeq to the uncurried form. Bisecting by replacing the rest of the proof with sorry pinned it to that single term. Removing classical alone did not help.