ext
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 σ))
σ : Semisentence ℒₒᵣ 1
⊢ Part.map (fun x => ()) (provableFn T (~[→ ⸢σ⸣].hom σ)) =
    Part.assert ((fun σ => T ⊢! ~[→ ⸢σ⸣].hom σ) σ) fun x => Part.some ()
case H
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 σ))
σ : Semisentence ℒₒᵣ 1
a✝ : Unit
⊢ a✝ ∈ Part.map (fun x => ()) (provableFn T (~[→ ⸢σ⸣].hom σ)) ↔
    a✝ ∈ Part.assert ((fun σ => T ⊢! ~[→ ⸢σ⸣].hom σ) σ) fun x => Part.some ()