simp [hssbs]
T : Theory ℒₒᵣ
inst✝² : 𝐄𝐐 ≼ T
inst✝¹ : 𝐏𝐀⁻ ≼ T
inst✝ : SigmaOneSound T
θ : Semisentence ℒₒᵣ 1
M : Type
x✝⁵ : Zero M
x✝⁴ : One M
x✝³ : Add M
x✝² : Mul M
x✝¹ : LT M
x✝ : M ⊧ₘ* T
this : M ⊧ₘ* 𝐏𝐀⁻
hssbs :
  ∀ (σ π : Semisentence ℒₒᵣ 1) (z : M), (Evalbm M ![z, ↑(encode σ), ↑(encode π)]) ssbs ↔ z = ↑(encode ([→ ⸢π⸣].hom σ))
⊢ (∀ (z : M), (Evalbm M ![z, ↑(encode (diag θ)), ↑(encode (diag θ))]) ssbs → (Evalbm M ![z]) θ) ↔
    (Evalbm M ![↑(encode ([→ ⸢diag θ⸣].hom (diag θ)))]) θ
no goals