Lean Computable₂ hang: split inline .to₂ terms into standalone lemmas

Building a Computable₂ fun σ i => decide (...) && !decide (...) proof inline as one big (Primrec.and.to_comp.comp (...).decide.to_comp.comp (... .pair ...)).to₂ term and passing it to a list_any-style combinator made the elaborator hang for minutes. The fix was a standalone lemma with the exact Computable₂ fun (σ : List Bool) (i : ℕ) => ... statement. Prove it with have steps typed over the pair, Computable fun p : List Bool × ℕ => ..., and use the two-argument form Primrec₂.to_comp.comp h1 h2 (e.g. Primrec.nat_lt.decide.to_comp.comp h1 h2) instead of .comp (h1.pair h2). The whole 570-line file then elaborated in about 3 seconds.