rintro ⟨b⟩
case mp
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : DecidablePred T
inst✝¹ : SigmaOneSound T
inst✝ : T.Computable
k : ℕ
f : Vector ℕ k →. ℕ
hf : Nat.Partrec' f
y : ℕ
v : Fin k → ℕ
σ : Sentence ℒₒᵣ := (Rew.substs (⸢y⸣ :> fun i => ⸢v i⸣)).hom (code (codeOfPartrec f))
sigma : Hierarchy 𝚺 1 σ
⊢ T ⊢! (Rew.substs (⸢y⸣ :> fun i => ⸢v i⸣)).hom (code (codeOfPartrec f)) → y ∈ f (Vector.ofFn v)
case mp.intro
T : Theory ℒₒᵣ
inst✝⁴ : 𝐄𝐐 ≼ T
inst✝³ : 𝐏𝐀⁻ ≼ T
inst✝² : DecidablePred T
inst✝¹ : SigmaOneSound T
inst✝ : T.Computable
k : ℕ
f : Vector ℕ k →. ℕ
hf : Nat.Partrec' f
y : ℕ
v : Fin k → ℕ
σ : Sentence ℒₒᵣ := (Rew.substs (⸢y⸣ :> fun i => ⸢v i⸣)).hom (code (codeOfPartrec f))
sigma : Hierarchy 𝚺 1 σ
b : T ⊢ (Rew.substs (⸢y⸣ :> fun i => ⸢v i⸣)).hom (code (codeOfPartrec f))
⊢ y ∈ f (Vector.ofFn v)