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

State before:
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : DecidablePred T
inst✝¹ : SigmaOneSound T
inst✝ : T.Computable
σ : Semisentence ℒₒᵣ 1
⊢ T ⊢! [→ ⸢σ⸣].hom ρ ↔ T ⊢! ~[→ ⸢σ⸣].hom σ
Tactic:
simpa[diagRefutation] using pred_representation T (diagRefutation_re T) (x := σ)
State after:
no goals