rintro (H | H)
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : SigmaOneSound T
inst✝¹ : DecidablePred T
inst✝ : T.Computable
⊢ ¬(T ⊢! G ∨ T ⊢! ~G)
case inl
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
⊢ False