simpa[System.Undecidable, not_or] using this
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : SigmaOneSound T
inst✝¹ : DecidablePred T
inst✝ : T.Computable
this : ¬(T ⊢! G ∨ T ⊢! ~G)
⊢ Undecidable T G
no goals