have : Nat.Partrec' (f' : Vector ℕ 2 →. ℕ) :=
  Nat.Partrec'.part_iff.mpr <| Computable.partrec <|
      (Primrec.option_get!).to_comp.comp <|
        Computable.option_bind
          (Computable.decode.comp .vector_head) <|
            Computable.option_map
              (Computable.decode.comp $ Computable.vector_head.comp $ Computable.vector_tail.comp .fst) <|
                Computable.encode.comp₂ <| hf.comp₂ (Computable.snd.comp₂ .left) .right
T : Theory ℒₒᵣ
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : 𝐏𝐀⁻ ≼ T
inst✝⁵ : DecidablePred T
inst✝⁴ : SigmaOneSound T
inst✝³ : T.Computable
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
hf : Computable₂ f
a : α
b : β
f' : Vector ℕ 2 → ℕ :=
  fun v => ((decode v.head).bind fun x => Option.map (fun y => encode (f x y)) (decode v.tail.head)).get!
⊢ T ⊢! (“∀' (!([→ #0, ⸢a⸣, ⸢b⸣].hom (graphTotal₂ f)) ↔ #0 = !!⸢f a b⸣)”)
T : Theory ℒₒᵣ
inst✝⁷ : 𝐄𝐐 ≼ T
inst✝⁶ : 𝐏𝐀⁻ ≼ T
inst✝⁵ : DecidablePred T
inst✝⁴ : SigmaOneSound T
inst✝³ : T.Computable
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
hf : Computable₂ f
a : α
b : β
f' : Vector ℕ 2 → ℕ :=
  fun v => ((decode v.head).bind fun x => Option.map (fun y => encode (f x y)) (decode v.tail.head)).get!
this : Nat.Partrec' ↑f'
⊢ T ⊢! (“∀' (!([→ #0, ⸢a⸣, ⸢b⸣].hom (graphTotal₂ f)) ↔ #0 = !!⸢f a b⸣)”)