exact ⟨x, by simpa using hx, by simpa[Matrix.comp_vecCons'] using pval_of_pval_nat_of_sigma_one hp h⟩
case intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
n✝ : ℕ
p✝ : Semiformula ℒₒᵣ Empty (n✝ + 1)
hp : Hierarchy 𝚺 1 p✝
e : Fin n✝ → ℕ
t : Semiterm ℒₒᵣ Empty n✝
pt : (Rew.bShift t).Positive
x : ℕ
hx : x < Semiterm.val (standardModel ℕ) e Empty.elim t
h : (Semiformula.Eval (standardModel ℕ) (x :> e) Empty.elim) p✝
⊢ ∃ x < ↑(Semiterm.valm ℕ (fun x => e x) Empty.elim t),
    (Semiformula.Eval (standardModel M) (x :> fun x => ↑(e x)) Empty.elim) p✝
no goals