have : T ⊢! ~G ⟷ (provableSentence T)/[⸢G⸣] := Gentzen.not_contra! (goedel_spec T)
case inr
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : SigmaOneSound T
inst✝¹ : DecidablePred T
inst✝ : T.Computable
H : T ⊢! ~G
⊢ False
case inr
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : SigmaOneSound T
inst✝¹ : DecidablePred T
inst✝ : T.Computable
H : T ⊢! ~G
this : T ⊢! ~G ⟷ [→ ⸢G⸣].hom (provableSentence T)
⊢ False