simp [goedelNumber_def,
  fixpoint_eq, Semiformula.eval_rew,
  Function.comp, Matrix.comp_vecCons',
  Matrix.constant_eq_vec₂,
  Model.numeral_eq_natCast,
  Matrix.constant_eq_singleton]
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 σ))
⊢ (Evalbm M ![]) (fixpoint θ) ↔
    ∀ (z : M), (Evalbm M ![z, ↑(encode (diag θ)), ↑(encode (diag θ))]) ssbs → (Evalbm M ![z]) θ
no goals