have : Partrec fun σ : Semisentence ℒₒᵣ 1 ↦ (provableFn T (~σ/[⸢σ⸣])).map (fun _ ↦ ()) :=
  Partrec.map
    ((provableFn_partrec T).comp <| Primrec.to_comp
      <| (Semiformula.neg_primrec (L := ℒₒᵣ)).comp
      <| (Semiformula.substs₁_primrec (L := ℒₒᵣ)).comp
        ((Semiterm.Operator.const_primrec (L := ℒₒᵣ)).comp
          <| (Semiterm.Operator.numeral_primrec (L := ℒₒᵣ)).comp .encode) .id)
    (.const ())
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : DecidablePred T
inst✝¹ : SigmaOneSound T
inst✝ : T.Computable
⊢ RePred fun σ => T ⊢! ~[→ ⸢σ⸣].hom σ
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : DecidablePred T
inst✝¹ : SigmaOneSound T
inst✝ : T.Computable
this : Partrec fun σ => Part.map (fun x => ()) (provableFn T (~[→ ⸢σ⸣].hom σ))
⊢ RePred fun σ => T ⊢! ~[→ ⸢σ⸣].hom σ