simpa [f', Matrix.comp_vecCons' (fun x : ℕ => (⸢x⸣ : Semiterm ℒₒᵣ Empty 1)),
  Matrix.constant_eq_singleton, graphTotal₂] using
    provable_computable_code_uniq T this ![encode a, encode 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⸣)”)
no goals