Theorem: LO.FirstOrder.Arith.FirstIncompleteness.SelfReference.goedel_spec (Logic/FirstOrder/Incompleteness/SelfReference.lean)

State before:
T : Theory ℒₒᵣ
inst✝² : 𝐄𝐐 ≼ T
inst✝¹ : 𝐏𝐀⁻ ≼ T
inst✝ : SigmaOneSound T
⊢ T ⊢! G ⟷ ~[→ ⸢G⸣].hom (provableSentence T)
Tactic:
simpa using SelfReference.main T (~provableSentence T)
State after:
no goals