haveI : M ⊧ₘ* 𝐏𝐀⁻ := ModelsTheory.of_provably_subtheory M 𝐏𝐀⁻ T inferInstance (by assumption)
M✝ : Type u_1
inst✝⁷ : Zero M✝
inst✝⁶ : One M✝
inst✝⁵ : Add M✝
inst✝⁴ : Mul M✝
inst✝³ : LT M✝
inst✝² : M✝ ⊧ₘ* 𝐏𝐀⁻
T : Theory ℒₒᵣ
inst✝¹ : 𝐄𝐐 ≼ T
inst✝ : 𝐏𝐀⁻ ≼ T
σ : Sentence ℒₒᵣ
hσ : Hierarchy 𝚺 1 σ
H : ℕ ⊧ₘ σ
M : Type
x✝⁵ : Zero M
x✝⁴ : One M
x✝³ : Add M
x✝² : Mul M
x✝¹ : LT M
x✝ : M ⊧ₘ* T
⊢ M ⊧ₘ σ
M✝ : Type u_1
inst✝⁷ : Zero M✝
inst✝⁶ : One M✝
inst✝⁵ : Add M✝
inst✝⁴ : Mul M✝
inst✝³ : LT M✝
inst✝² : M✝ ⊧ₘ* 𝐏𝐀⁻
T : Theory ℒₒᵣ
inst✝¹ : 𝐄𝐐 ≼ T
inst✝ : 𝐏𝐀⁻ ≼ T
σ : Sentence ℒₒᵣ
hσ : Hierarchy 𝚺 1 σ
H : ℕ ⊧ₘ σ
M : Type
x✝⁵ : Zero M
x✝⁴ : One M
x✝³ : Add M
x✝² : Mul M
x✝¹ : LT M
x✝ : M ⊧ₘ* T
this : M ⊧ₘ* 𝐏𝐀⁻
⊢ M ⊧ₘ σ