constructor
ξ : Type u_1
n : ℕ
M : Type u_2
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
t : Semiterm ℒₒᵣ ξ n
p : Semiformula ℒₒᵣ ξ (n + 1)
e : Fin n → M
ε : ξ → M
⊢ (∃ x < Semiterm.val (standardModel M) e ε t,
      x ∈ Semiterm.val (standardModel M) e ε t ∧ (Semiformula.Eval (standardModel M) (x :> e) ε) p) ↔
    ∃ x ∈ Semiterm.valm M e ε t, (Semiformula.Evalm M (x :> e) ε) p
case mp
ξ : Type u_1
n : ℕ
M : Type u_2
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
t : Semiterm ℒₒᵣ ξ n
p : Semiformula ℒₒᵣ ξ (n + 1)
e : Fin n → M
ε : ξ → M
⊢ (∃ x < Semiterm.val (standardModel M) e ε t,
      x ∈ Semiterm.val (standardModel M) e ε t ∧ (Semiformula.Eval (standardModel M) (x :> e) ε) p) →
    ∃ x ∈ Semiterm.valm M e ε t, (Semiformula.Evalm M (x :> e) ε) p

case mpr
ξ : Type u_1
n : ℕ
M : Type u_2
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
t : Semiterm ℒₒᵣ ξ n
p : Semiformula ℒₒᵣ ξ (n + 1)
e : Fin n → M
ε : ξ → M
⊢ (∃ x ∈ Semiterm.valm M e ε t, (Semiformula.Evalm M (x :> e) ε) p) →
    ∃ x < Semiterm.val (standardModel M) e ε t,
      x ∈ Semiterm.val (standardModel M) e ε t ∧ (Semiformula.Eval (standardModel M) (x :> e) ε) p