have : Definable ℒₒᵣ (Γ, m + 1) (fun v ↦ ∃ x < f v, x ∈ f v ∧ P v x) :=
  .bex_lt hf (.and (by simpa using Definable.comp₂ (by simp) (hf.retraction _) (by simp)) h)
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
Γ : SigmaPiDelta
m : ℕ
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction ℒₒᵣ (𝚺, m + 1) f
h : Definable ℒₒᵣ (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
⊢ Definable ℒₒᵣ (Γ, m + 1) fun v => ∃ x ∈ f v, P v x
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
Γ : SigmaPiDelta
m : ℕ
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction ℒₒᵣ (𝚺, m + 1) f
h : Definable ℒₒᵣ (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
this : Definable ℒₒᵣ (Γ, m + 1) fun v => ∃ x < f v, x ∈ f v ∧ P v x
⊢ Definable ℒₒᵣ (Γ, m + 1) fun v => ∃ x ∈ f v, P v x