have h₁ : T ⊢! ~(provableSentence T)/[⸢G⸣] := System.and_left! (goedel_spec T) ⨀ H
case inl
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : SigmaOneSound T
inst✝¹ : DecidablePred T
inst✝ : T.Computable
H : T ⊢! G
⊢ False
case inl
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : SigmaOneSound T
inst✝¹ : DecidablePred T
inst✝ : T.Computable
H : T ⊢! G
h₁ : T ⊢! ~[→ ⸢G⸣].hom (provableSentence T)
⊢ False