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