simp [Semiformula.eval_rewriteMap, hhp]
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
P : M → Prop
zero : P 0
succ : ∀ (x : M), P x → P (x + 1)
p : Semiformula ℒₒᵣ M 1
hp : p.Open
hhp : ∀ (x : M), P x ↔ (Semiformula.Evalm M ![x] id) p
this : Inhabited M
x : M
⊢ P x ↔ (Semiformula.Evalm M ![x] p.fvEnumInv) ((Rew.rewriteMap p.fvEnum).hom p)
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
P : M → Prop
zero : P 0
succ : ∀ (x : M), P x → P (x + 1)
p : Semiformula ℒₒᵣ M 1
hp : p.Open
hhp : ∀ (x : M), P x ↔ (Semiformula.Evalm M ![x] id) p
this : Inhabited M
x : M
⊢ (Semiformula.Evalm M ![x] id) p ↔ (Semiformula.Eval (standardModel M) ![x] fun x => p.fvEnumInv (p.fvEnum x)) p