simp [Semiformula.fvEnumInv_fvEnum hz]
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 z : M
hz : p.fvar? z
⊢ id z = (fun x => p.fvEnumInv (p.fvEnum x)) z
no goals