calc
  Evalbm M ![] (fixpoint θ)
  ↔ ∀ z, Evalbm M ![z, encode (diag θ), encode (diag θ)] ssbs → Evalbm M ![z] θ := by 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]
_ ↔ Evalbm M ![encode “!(diag θ) !!(⸢diag θ⸣ : Semiterm ℒₒᵣ Empty 0)”] θ        := by simp [hssbs]
_ ↔ Evalbm M ![encode (fixpoint θ)] θ                                           := by rfl
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 θ) ↔ (Evalbm M ![↑(encode (fixpoint θ))]) θ
no goals