rcases standardModel_unique M s
T : Theory ℒₒᵣ
inst✝ : 𝐄𝐐 ≼ T
σ : Sentence ℒₒᵣ
H :
  ∀ (M : Type w) [inst : Zero M] [inst_1 : One M] [inst_2 : Add M] [inst_3 : Mul M] [inst_4 : LT M] [inst_5 : M ⊧ₘ* T],
    M ⊧ₘ σ
M : Type ?u.361593
x✝⁶ : Zero M
x✝⁵ : One M
x✝⁴ : Add M
x✝³ : Mul M
x✝² : LT M
s : Structure ℒₒᵣ M
x✝¹ : Structure.ORing ℒₒᵣ M
x✝ : M ⊧ₘ* T
⊢ M ⊧ₘ σ
case refl
T : Theory ℒₒᵣ
inst✝ : 𝐄𝐐 ≼ T
σ : Sentence ℒₒᵣ
H :
  ∀ (M : Type w) [inst : Zero M] [inst_1 : One M] [inst_2 : Add M] [inst_3 : Mul M] [inst_4 : LT M] [inst_5 : M ⊧ₘ* T],
    M ⊧ₘ σ
M : Type ?u.361593
x✝⁶ : Zero M
x✝⁵ : One M
x✝⁴ : Add M
x✝³ : Mul M
x✝² : LT M
x✝¹ : Structure.ORing ℒₒᵣ M
x✝ : M ⊧ₘ* T
⊢ M ⊧ₘ σ