simpa [goedelNumber_def, Model.numeral_eq_natCast, models_iff, Semiformula.eval_substs, Matrix.comp_vecCons', Matrix.constant_eq_singleton] using
fun σ π => consequence_iff'.mp (sound₀! (ssbs_spec (T := T) σ π)) M
T : Theory ℒₒᵣ
inst✝² : 𝐄𝐐 ≼ T
inst✝¹ : 𝐏𝐀⁻ ≼ T
inst✝ : SigmaOneSound T
θ : Semisentence ℒₒᵣ 1
M : Type ?u.32377
x✝⁵ : Zero M
x✝⁴ : One M
x✝³ : Add M
x✝² : Mul M
x✝¹ : LT M
x✝ : M ⊧ₘ* T
this : M ⊧ₘ* 𝐏𝐀⁻
⊢ ∀ (σ π : Semisentence ℒₒᵣ 1) (z : M), (Evalbm M ![z, ↑(encode σ), ↑(encode π)]) ssbs ↔ z = ↑(encode ([→ ⸢π⸣].hom σ))
no goals