simpa [f', Matrix.comp_vecCons', Matrix.constant_eq_singleton] using
  provable_computable_code_uniq T this ![encode a]
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 : α
f' : Vector ℕ 1 → ℕ := fun x => (Option.map (fun x => encode (f x)) (decode x.head)).get!
this : Nat.Partrec' ↑f'
⊢ T ⊢! (“∀' (!([→ #0, ⸢a⸣].hom (graphTotal f)) ↔ #0 = !!⸢f a⸣)”)
no goals