simp [←Matrix.constant_eq_singleton', Semiformula.eval_rewriteMap]
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
inst✝⁵ : M ⊧ₘ* 𝐏𝐀⁻
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
p : Semiformula L ℕ 1
hp : Hierarchy Γ.alt m p
v : ℕ → M
H0 : (Semiformula.Eval inst✝³ ![0] v) p
Hsucc : ∀ (x : M), (Semiformula.Eval inst✝³ ![x] v) p → (Semiformula.Eval inst✝³ ![x + 1] v) p
x✝ : M
x : Fin 1 → M
⊢ (fun x => ¬(Semiformula.Evalm M ![x] v) p) (x 0) ↔ (Semiformula.Evalm M x id) (~(Rew.rewriteMap v).hom p)
no goals