have : T ⊢! (provableSentence T)/[⸢G⸣] := System.and_left! this ⨀ H
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
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)
this : T ⊢! [→ ⸢G⸣].hom (provableSentence T)
⊢ False