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

State before:
T : Theory ℒₒᵣ
inst✝² : 𝐄𝐐 ≼ T
inst✝¹ : 𝐏𝐀⁻ ≼ T
inst✝ : SigmaOneSound T
θ σ : Semisentence ℒₒᵣ 1
⊢ [→ ⸢σ⸣].hom (diag θ) = ∀' ([→ #0, ⸢σ⸣, ⸢σ⸣].hom ssbs ⟶ [→ #0].hom θ)
Tactic:
simp [diag, Rew.q_substs, ←Rew.hom_comp_app, Rew.substs_comp_substs]
State after:
no goals