intro x hx
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 : M → Prop
zero : P 0
succ : ∀ (x : M), P x → P (x + 1)
p : HSemiformula L M 1 (Γ.coe, m)
hp : DefinedWithParam (fun v => P (v 0)) p
this : Inhabited M
x : M
⊢ Function.funEqOn p.val.fvar? (fun x => p.val.fvEnumInv (p.val.fvEnum x)) id
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 : M → Prop
zero : P 0
succ : ∀ (x : M), P x → P (x + 1)
p : HSemiformula L M 1 (Γ.coe, m)
hp : DefinedWithParam (fun v => P (v 0)) p
this : Inhabited M
x✝ x : M
hx : p.val.fvar? x
⊢ (fun x => p.val.fvEnumInv (p.val.fvEnum x)) x = id x