rintro rfl
case mpr
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : DecidablePred T
inst✝¹ : SigmaOneSound T
inst✝ : T.Computable
k : ℕ
f : Vector ℕ k → ℕ
hf : Nat.Partrec' ↑f
v : Fin k → ℕ
M : Type
x✝⁵ : Zero M
x✝⁴ : One M
x✝³ : Add M
x✝² : Mul M
x✝¹ : LT M
x✝ : M ⊧ₘ* T
this : M ⊧ₘ* 𝐏𝐀⁻
Hfv : (Semiformula.Evalbm M (↑(f (Vector.ofFn v)) :> fun x => ↑(v x))) (code (codeOfPartrec ↑f))
x : M
⊢ x = ↑(f (Vector.ofFn v)) →
    (Semiformula.Eval (standardModel M) (x :> fun i => ↑(v i)) Empty.elim) (code (codeOfPartrec ↑f))
case mpr
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : DecidablePred T
inst✝¹ : SigmaOneSound T
inst✝ : T.Computable
k : ℕ
f : Vector ℕ k → ℕ
hf : Nat.Partrec' ↑f
v : Fin k → ℕ
M : Type
x✝⁵ : Zero M
x✝⁴ : One M
x✝³ : Add M
x✝² : Mul M
x✝¹ : LT M
x✝ : M ⊧ₘ* T
this : M ⊧ₘ* 𝐏𝐀⁻
Hfv : (Semiformula.Evalbm M (↑(f (Vector.ofFn v)) :> fun x => ↑(v x))) (code (codeOfPartrec ↑f))
⊢ (Semiformula.Eval (standardModel M) (↑(f (Vector.ofFn v)) :> fun i => ↑(v i)) Empty.elim) (code (codeOfPartrec ↑f))