Post-composing Nat.RecursiveIn functions with a merely Computable map

Mathlib's Nat.RecursiveIn has no typed composition lemma. A helper that only post-composes with Primrec₂ maps is not enough once the map depends on a Computable (not primitive recursive) approximation. A general version works: first get n ↦ (g n).map (Nat.pair n) from Nat.RecursiveIn.pair with id, simplifying Seq.seq via simp. Then get Nat.Partrec fun m => Part.some (k m.unpair.1 m.unpair.2) from Partrec.nat_iff.1 (hk.comp ...) and lift it with .recursiveIn. Finish with Nat.RecursiveIn.comp and prove the Part equality by Part.ext plus simp [Part.mem_bind_iff, Part.mem_map_iff, eq_comm]; without eq_comm, simp leaves y = k n a vs k n a = y.