exact
  ⟨fun b ↦ (Gentzen.inconsistent_of_provable_and_refutable! b (h.mp b)).not_con (consistent_of_sigmaOneSound T),
   fun b ↦ (Gentzen.inconsistent_of_provable_and_refutable! (h.mpr b) b).not_con (consistent_of_sigmaOneSound T)⟩
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : DecidablePred T
inst✝¹ : SigmaOneSound T
inst✝ : T.Computable
h : T ⊢! γ ↔ T ⊢! ~γ
⊢ System.Undecidable T γ
no goals