chore: cleanup proof of Nat.Partrec.Code.rec_prim (#10978)

This is in preparation for a fix to be performed on `nightly-testing`. It restores the proof structure to something more similar to the original lean 3 proof.



Co-authored-by: Mario Carneiro <di.gama@gmail.com>

Mathlib/Computability/Partrec.lean

@@ -542,6 +542,8 @@ variable {α : Type*} {β : Type*} {γ : Type*} {δ : Type*} {σ : Type*}
 
 variable [Primcodable α] [Primcodable β] [Primcodable γ] [Primcodable δ] [Primcodable σ]
 
+theorem mk {f : α → β → σ} (hf : Computable fun p : α × β => f p.1 p.2) : Computable₂ f := hf
+
 nonrec theorem comp {f : β → γ → σ} {g : α → β} {h : α → γ} (hf : Computable₂ f)
     (hg : Computable g) (hh : Computable h) : Computable fun a => f (g a) (h a) :=
   hf.comp (hg.pair hh)