diff --git a/Arithmetization/Basic/IOpen.lean b/Arithmetization/Basic/IOpen.lean
index c5663ea..4fbcaa3 100644
--- a/Arithmetization/Basic/IOpen.lean
+++ b/Arithmetization/Basic/IOpen.lean
@@ -7,13 +7,13 @@ namespace Arith
 
 noncomputable section
 
-variable {M : Type} [Zero M] [One M] [Add M] [Mul M] [LT M] [𝐏𝐀⁻.Mod M]
+variable {M : Type} [Zero M] [One M] [Add M] [Mul M] [LT M] [M ⊧ₘ* 𝐏𝐀⁻]
 
 namespace Model
 
 section IOpen
 
-variable [𝐈open.Mod M]
+variable [M ⊧ₘ* 𝐈open]
 
 @[elab_as_elim]
 lemma open_induction {P : M → Prop}
@@ -626,16 +626,16 @@ end IOpen
 
 section polynomial_induction
 
-variable [𝐈open.Mod M]
+variable [M ⊧ₘ* 𝐈open]
 variable {L : Language} [L.ORing] [Structure L M] [Structure.ORing L M] [Structure.Monotone L M]
 
 @[elab_as_elim]
-lemma hierarchy_polynomial_induction (Γ ν) [(Theory.indScheme L (Arith.Hierarchy Γ ν)).Mod M]
-    {P : M → Prop} (hP : DefinablePred L Γ ν P)
+lemma hierarchy_polynomial_induction (Γ n) [M ⊧ₘ* Theory.indScheme L (Arith.Hierarchy Γ n)]
+    {P : M → Prop} (hP : DefinablePred L Γ n P)
     (zero : P 0) (even : ∀ x > 0, P x → P (2 * x)) (odd : ∀ x, P x → P (2 * x + 1)) : ∀ x, P x := by
   intro x; induction x using order_induction_h
   · exact Γ
-  · exact ν
+  · exact n
   · exact hP
   case inst => exact inferInstance
   case inst => exact inferInstance
@@ -649,15 +649,15 @@ lemma hierarchy_polynomial_induction (Γ ν) [(Theory.indScheme L (Arith.Hierarc
 
 end polynomial_induction
 
-@[elab_as_elim] lemma hierarchy_polynomial_induction_oRing_sigma₀ [𝐈𝚺₀.Mod M] {P : M → Prop} (hP : DefinablePred ℒₒᵣ Σ 0 P)
+@[elab_as_elim] lemma hierarchy_polynomial_induction_oRing_sigma₀ [M ⊧ₘ* 𝐈𝚺₀] {P : M → Prop} (hP : DefinablePred ℒₒᵣ Σ 0 P)
     (zero : P 0) (even : ∀ x > 0, P x → P (2 * x)) (odd : ∀ x, P x → P (2 * x + 1)) : ∀ x, P x :=
   hierarchy_polynomial_induction Σ 0 hP zero even odd
 
-@[elab_as_elim] lemma hierarchy_polynomial_induction_oRing_sigma₁ [𝐈𝚺₁.Mod M] {P : M → Prop} (hP : DefinablePred ℒₒᵣ Σ 1 P)
+@[elab_as_elim] lemma hierarchy_polynomial_induction_oRing_sigma₁ [M ⊧ₘ* 𝐈𝚺₁] {P : M → Prop} (hP : DefinablePred ℒₒᵣ Σ 1 P)
     (zero : P 0) (even : ∀ x > 0, P x → P (2 * x)) (odd : ∀ x, P x → P (2 * x + 1)) : ∀ x, P x :=
   hierarchy_polynomial_induction Σ 1 hP zero even odd
 
-@[elab_as_elim] lemma hierarchy_polynomial_induction_oRing_pi₁ [𝐈𝚷₁.Mod M] {P : M → Prop} (hP : DefinablePred ℒₒᵣ Π 1 P)
+@[elab_as_elim] lemma hierarchy_polynomial_induction_oRing_pi₁ [M ⊧ₘ* 𝐈𝚷₁] {P : M → Prop} (hP : DefinablePred ℒₒᵣ Π 1 P)
     (zero : P 0) (even : ∀ x > 0, P x → P (2 * x)) (odd : ∀ x, P x → P (2 * x + 1)) : ∀ x, P x :=
   hierarchy_polynomial_induction Π 1 hP zero even odd
 
diff --git a/Arithmetization/Basic/Ind.lean b/Arithmetization/Basic/Ind.lean
index 155fe4e..d4b17a3 100644
--- a/Arithmetization/Basic/Ind.lean
+++ b/Arithmetization/Basic/Ind.lean
@@ -2,8 +2,6 @@ import Arithmetization.Basic.PeanoMinus
 
 namespace LO.FirstOrder
 
-attribute [simp] Theory.Mod.modelsTheory
-
 namespace Arith
 
 namespace Theory
@@ -40,18 +38,18 @@ variable {M : Type} [Zero M] [One M] [Add M] [Mul M] [LT M]
 
 section
 
-variable [𝐏𝐀⁻.Mod M] {L : Language} [L.ORing] [Structure L M] [Structure.ORing L M] [Structure.Monotone L M]
+variable [M ⊧ₘ* 𝐏𝐀⁻] {L : Language} [L.ORing] [Structure L M] [Structure.ORing L M] [Structure.Monotone L M]
 
 section IndScheme
 
-variable {C : Semiformula L ℕ 1 → Prop} [(Theory.indScheme L C).Mod M]
+variable {C : Semiformula L ℕ 1 → Prop} [M ⊧ₘ* Theory.indScheme L C]
 
 private lemma induction_eval {p : Semiformula L ℕ 1} (hp : C p) (v) :
     Semiformula.Eval! M ![0] v p →
     (∀ x, Semiformula.Eval! M ![x] v p → Semiformula.Eval! M ![x + 1] v p) →
     ∀ x, Semiformula.Eval! M ![x] v p := by
   have : M ⊧ₘ (∀ᶠ* succInd p) :=
-    Theory.Mod.models (T := Theory.indScheme _ C) M (by simpa using Theory.mem_indScheme_of_mem hp)
+    ModelsTheory.models (T := Theory.indScheme _ C) M (by simpa using Theory.mem_indScheme_of_mem hp)
   simp [models_iff, succInd, Semiformula.eval_substs,
     Semiformula.eval_rew_q Rew.toS, Function.comp, Matrix.constant_eq_singleton] at this
   exact this v
@@ -68,7 +66,7 @@ end IndScheme
 
 section neg
 
-variable (Γ : Polarity) (s : ℕ) [(Theory.indScheme L (Arith.Hierarchy Γ s)).Mod M]
+variable (Γ : Polarity) (s : ℕ) [M ⊧ₘ* Theory.indScheme L (Arith.Hierarchy Γ s)]
 
 @[elab_as_elim]
 lemma induction_h {P : M → Prop} (hP : DefinablePred L Γ s P)
@@ -142,7 +140,7 @@ lemma models_indScheme_alt : M ⊧ₘ* Theory.indScheme L (Arith.Hierarchy Γ.al
           by intro x; simp [←Matrix.constant_eq_singleton', Semiformula.eval_rewriteMap]⟩
   exact this H0 Hsucc x
 
-instance : (Theory.indScheme L (Arith.Hierarchy Γ.alt s)).Mod M := ⟨models_indScheme_alt Γ s⟩
+instance : M ⊧ₘ* Theory.indScheme L (Arith.Hierarchy Γ.alt s) := models_indScheme_alt Γ s
 
 lemma least_number_h {P : M → Prop} (hP : DefinablePred L Γ s P)
     {x} (h : P x) : ∃ y, P y ∧ ∀ z < y, ¬P z := by
@@ -169,59 +167,59 @@ lemma least_number_h {P : M → Prop} (hP : DefinablePred L Γ s P)
 
 end neg
 
-instance [(Theory.indScheme L (Arith.Hierarchy Σ s)).Mod M] :
-    (Theory.indScheme L (Arith.Hierarchy Γ s)).Mod M := by
+instance [M ⊧ₘ* Theory.indScheme L (Arith.Hierarchy Σ s)] :
+    M ⊧ₘ* Theory.indScheme L (Arith.Hierarchy Γ s) := by
   rcases Γ
   · exact inferInstance
-  · exact ⟨models_indScheme_alt Σ s⟩
+  · exact models_indScheme_alt Σ s
 
 end
 
-def mod_iOpen_of_mod_indH (Γ s) [(𝐈𝐍𝐃Γ s).Mod M] : 𝐈open.Mod M :=
-  Theory.Mod.of_ss (T₁ := 𝐈𝐍𝐃Γ s) M (Set.union_subset_union_right _ (Theory.indScheme_subset Hierarchy.of_open))
+def mod_iOpen_of_mod_indH (Γ n) [M ⊧ₘ* 𝐈𝐍𝐃Γ n] : M ⊧ₘ* 𝐈open :=
+  ModelsTheory.of_ss (U := 𝐈𝐍𝐃Γ n) inferInstance
+    (Set.union_subset_union_right _ (Theory.indScheme_subset Hierarchy.of_open))
 
-def mod_iSigma_of_le {s₁ s₂} (h : s₁ ≤ s₂) [(𝐈𝚺 s₂).Mod M] : (𝐈𝚺 s₁).Mod M :=
-  Theory.Mod.of_ss M (Theory.iSigma_subset_mono h)
+def mod_iSigma_of_le {n₁ n₂} (h : n₁ ≤ n₂) [M ⊧ₘ* 𝐈𝚺 n₂] : M ⊧ₘ* 𝐈𝚺 n₁ :=
+  ModelsTheory.of_ss inferInstance (Theory.iSigma_subset_mono h)
 
-instance [𝐈open.Mod M] : 𝐏𝐀⁻.Mod M := Theory.Mod.of_add_left M 𝐏𝐀⁻ (Theory.indScheme _ Semiformula.Open)
+instance [M ⊧ₘ* 𝐈open] : M ⊧ₘ* 𝐏𝐀⁻ := ModelsTheory.of_add_left M 𝐏𝐀⁻ (Theory.indScheme _ Semiformula.Open)
 
-instance [𝐈𝚺₀.Mod M] : 𝐈open.Mod M := mod_iOpen_of_mod_indH Σ 0
+instance [M ⊧ₘ* 𝐈𝚺₀] : M ⊧ₘ* 𝐈open := mod_iOpen_of_mod_indH Σ 0
 
-instance [𝐈𝚺₁.Mod M] : 𝐈𝚺₀.Mod M := mod_iSigma_of_le (show 0 ≤ 1 from by simp)
+instance [M ⊧ₘ* 𝐈𝚺₁] : M ⊧ₘ* 𝐈𝚺₀ := mod_iSigma_of_le (show 0 ≤ 1 from by simp)
 
-instance [(𝐈𝚺 ν).Mod M] : (𝐈𝐍𝐃 Γ ν).Mod M := by
-  rcases Γ
-  · exact inferInstance
-  · haveI : 𝐏𝐀⁻.Mod M := Arith.mod_peanoMinus_of_mod_indH (Γ := Σ) (ν := ν)
-    exact inferInstance
+instance [M ⊧ₘ* 𝐈𝚺 n] : M ⊧ₘ* 𝐈𝚷 n :=
+  haveI : M ⊧ₘ* 𝐏𝐀⁻ := Arith.models_peanoMinus_of_models_indH Σ n
+  inferInstance
+
+instance [M ⊧ₘ* 𝐈𝚷 n] : M ⊧ₘ* 𝐈𝚺 n :=
+  haveI : M ⊧ₘ* 𝐏𝐀⁻ := Arith.models_peanoMinus_of_models_indH Π n
+  by simp [*]; simpa [Theory.iPi] using models_indScheme_alt (L := ℒₒᵣ) (M := M) Π n
 
-instance [(𝐈𝚷 ν).Mod M] : (𝐈𝚺 ν).Mod M :=
-  haveI : 𝐏𝐀⁻.Mod M := Arith.mod_peanoMinus_of_mod_indH (Γ := Π) (ν := ν)
-  Theory.Mod.of_models (by simpa [Theory.iPi] using models_indScheme_alt (M := M) Π ν)
+lemma models_iSigma_iff_models_iPi {n} : M ⊧ₘ* 𝐈𝚺 n ↔ M ⊧ₘ* 𝐈𝚷 n :=
+  ⟨fun _ ↦ inferInstance, fun _ ↦ inferInstance⟩
 
-lemma models_iSigma_iff_models_iPi : M ⊧ₘ* 𝐈𝚺 ν ↔ M ⊧ₘ* 𝐈𝚷 ν :=
-  ⟨fun h ↦ by haveI : (𝐈𝚺 ν).Mod M := ⟨h⟩; exact Theory.Mod.modelsTheory M _,
-   fun h ↦ by haveI : (𝐈𝚷 ν).Mod M := ⟨h⟩; exact Theory.Mod.modelsTheory M _⟩
+instance [M ⊧ₘ* 𝐈𝚺 n] : M ⊧ₘ* 𝐈𝐍𝐃Γ n := by rcases Γ <;> exact inferInstance
 
-@[elab_as_elim] lemma induction_iSigmaZero [𝐈𝚺₀.Mod M]
+@[elab_as_elim] lemma induction_iSigmaZero [M ⊧ₘ* 𝐈𝚺₀]
     {P : M → Prop} (hP : DefinablePred ℒₒᵣ Σ 0 P)
     (zero : P 0) (succ : ∀ x, P x → P (x + 1)) : ∀ x, P x := induction_h Σ 0 hP zero succ
 
-@[elab_as_elim] lemma induction_iSigmaOne [𝐈𝚺₁.Mod M]
+@[elab_as_elim] lemma induction_iSigmaOne [M ⊧ₘ* 𝐈𝚺₁]
     {P : M → Prop} (hP : DefinablePred ℒₒᵣ Σ 1 P)
     (zero : P 0) (succ : ∀ x, P x → P (x + 1)) : ∀ x, P x := induction_h Σ 1 hP zero succ
 
-@[elab_as_elim] lemma order_induction_iSigmaZero [𝐈𝚺₀.Mod M]
+@[elab_as_elim] lemma order_induction_iSigmaZero [M ⊧ₘ* 𝐈𝚺₀]
     {P : M → Prop} (hP : DefinablePred ℒₒᵣ Σ 0 P)
     (ind : ∀ x, (∀ y < x, P y) → P x) : ∀ x, P x :=
   order_induction_h Σ 0 hP ind
 
-@[elab_as_elim] lemma order_induction_iSigmaOne [𝐈𝚺₁.Mod M]
+@[elab_as_elim] lemma order_induction_iSigmaOne [M ⊧ₘ* 𝐈𝚺₁]
     {P : M → Prop} (hP : DefinablePred ℒₒᵣ Σ 1 P)
     (ind : ∀ x, (∀ y < x, P y) → P x) : ∀ x, P x :=
   order_induction_h Σ 1 hP ind
 
-lemma least_number_iSigmaZero [𝐈𝚺₀.Mod M] {P : M → Prop} (hP : DefinablePred ℒₒᵣ Σ 0 P)
+lemma least_number_iSigmaZero [M ⊧ₘ* 𝐈𝚺₀] {P : M → Prop} (hP : DefinablePred ℒₒᵣ Σ 0 P)
     {x} (h : P x) : ∃ y, P y ∧ ∀ z < y, ¬P z :=
   least_number_h Σ 0 hP h
 
diff --git a/Arithmetization/Basic/PeanoMinus.lean b/Arithmetization/Basic/PeanoMinus.lean
index 48147f3..2d0cfb1 100644
--- a/Arithmetization/Basic/PeanoMinus.lean
+++ b/Arithmetization/Basic/PeanoMinus.lean
@@ -6,7 +6,7 @@ namespace Arith
 
 noncomputable section
 
-variable {M : Type} [Zero M] [One M] [Add M] [Mul M] [LT M] [𝐏𝐀⁻.Mod M]
+variable {M : Type} [Zero M] [One M] [Add M] [Mul M] [LT M] [M ⊧ₘ* 𝐏𝐀⁻]
 
 namespace Model
 
diff --git a/Arithmetization/Definability/Definability.lean b/Arithmetization/Definability/Definability.lean
index 98088b6..216b116 100644
--- a/Arithmetization/Definability/Definability.lean
+++ b/Arithmetization/Definability/Definability.lean
@@ -34,7 +34,7 @@ namespace Arith
 
 section definability
 
-variable {M : Type} [Zero M] [One M] [Add M] [Mul M] [LT M] [𝐏𝐀⁻.Mod M]
+variable {M : Type} [Zero M] [One M] [Add M] [Mul M] [LT M] [M ⊧ₘ* 𝐏𝐀⁻]
 variable {L : Language} [L.ORing] [Structure L M] [Structure.ORing L M] [Structure.Monotone L M]
 
 namespace Definability
diff --git a/Arithmetization/IDeltaZero/Basic.lean b/Arithmetization/IDeltaZero/Basic.lean
index 41ed547..6c6a8a2 100644
--- a/Arithmetization/IDeltaZero/Basic.lean
+++ b/Arithmetization/IDeltaZero/Basic.lean
@@ -9,13 +9,13 @@ namespace Arith
 
 noncomputable section
 
-variable {M : Type} [Nonempty M] [Zero M] [One M] [Add M] [Mul M] [LT M] [𝐏𝐀⁻.Mod M]
+variable {M : Type} [Nonempty M] [Zero M] [One M] [Add M] [Mul M] [LT M] [M ⊧ₘ* 𝐏𝐀⁻]
 
 namespace Model
 
 section ISigma₀
 
-variable [𝐈𝚺₀.Mod M]
+variable [M ⊧ₘ* 𝐈𝚺₀]
 
 
 end ISigma₀
diff --git a/Arithmetization/IDeltaZero/Exponential/Exp.lean b/Arithmetization/IDeltaZero/Exponential/Exp.lean
index dc9ba47..368c5a0 100644
--- a/Arithmetization/IDeltaZero/Exponential/Exp.lean
+++ b/Arithmetization/IDeltaZero/Exponential/Exp.lean
@@ -12,7 +12,7 @@ namespace Model
 
 section ISigma₀
 
-variable [𝐈𝚫₀.Mod M]
+variable [M ⊧ₘ* 𝐈𝚫₀]
 
 def ext (u z : M) : M := z / u % u
 
@@ -87,7 +87,8 @@ def Exp.Seqₛ.def : Δ₀-Sentence 3 := ⟨
       ∃[#0 < #4 + 1] (!extDef [#0, #1, #4] ∧ !extDef [2 * (#0 * #0), #1 * #1, #4])))”, by simp⟩
 
 lemma Exp.Seqₛ.defined : Δ₀-Relation₃ (Exp.Seqₛ : M → M → M → Prop) via Exp.Seqₛ.def := by
-  intro v; simp [Exp.Seqₛ.iff, Exp.Seqₛ.def, ppow2_defined.pval, ext_defined.pval, ←le_iff_lt_succ, sq]
+  intro v; simp [Exp.Seqₛ.iff, Exp.Seqₛ.def, ppow2_defined.pval,
+    ext_defined.pval, ←le_iff_lt_succ, sq, numeral_eq_natCast]
 
 lemma Exp.graph_iff (x y : M) :
     Exp x y ↔
@@ -110,7 +111,8 @@ def Exp.def : Δ₀-Sentence 2 := ⟨
       ∃[#0 < #4 * #4 + 1] (#0 ≠ 2 ∧ !ppow2Def [#0] ∧ !extDef [#3, #0, #2] ∧!extDef [#4, #0, #1])))”, by simp⟩
 
 lemma Exp.defined : Δ₀-Relation (Exp : M → M → Prop) via Exp.def := by
-  intro v; simp [Exp.graph_iff, Exp.def, ppow2_defined.pval, ext_defined.pval, Exp.Seqₛ.defined.pval, ←le_iff_lt_succ, pow_four, sq]
+  intro v; simp [Exp.graph_iff, Exp.def, ppow2_defined.pval, ext_defined.pval,
+    Exp.Seqₛ.defined.pval, ←le_iff_lt_succ, pow_four, sq, numeral_eq_natCast]
 
 instance exp_definable : DefinableRel ℒₒᵣ Σ 0 (Exp : M → M → Prop) := defined_to_with_param _ Exp.defined
 
@@ -682,7 +684,7 @@ end ISigma₀
 
 section ISigma₁
 
-variable [𝐈𝚺₁.Mod M]
+variable [M ⊧ₘ* 𝐈𝚺₁]
 
 namespace Exp
 
@@ -700,9 +702,7 @@ lemma range_exists_unique (x : M) : ∃! y, Exp x y := by
 
 end Exp
 
-def exponential (a : M) : M := Classical.choose! (Exp.range_exists_unique a)
-
-prefix:80 "exp " => exponential
+instance : _root_.Exp M := ⟨fun a ↦ Classical.choose! (Exp.range_exists_unique a)⟩
 
 section exponential
 
@@ -714,15 +714,15 @@ def expdef : Δ₀-Sentence 2 := ⟨“!Exp.def [#1, #0]”, by simp⟩
 
 -- #eval expdef.val
 
-lemma exp_defined : Δ₀-Function₁ (exponential : M → M) via expdef := by
+lemma exp_defined : Δ₀-Function₁ (Exp.exp : M → M) via expdef := by
   intro v; simp [expdef, exponential_graph, Exp.defined.pval]
 
-instance exponential_definable : DefinableFunction₁ ℒₒᵣ Σ 0 (exponential : M → M) := defined_to_with_param _ exp_defined
+instance exponential_definable : DefinableFunction₁ ℒₒᵣ Σ 0 (Exp.exp : M → M) := defined_to_with_param _ exp_defined
 
 lemma exponential_of_exp {a b : M} (h : Exp a b) : exp a = b :=
   Eq.symm <| exponential_graph.mpr h
 
-lemma exponential_inj : Function.Injective (exponential : M → M) := λ a _ H ↦
+lemma exponential_inj : Function.Injective (Exp.exp : M → M) := λ a _ H ↦
   (exp_exponential a).inj (exponential_graph.mp H)
 
 @[simp] lemma exp_zero : exp (0 : M) = 1 := exponential_of_exp (by simp)
diff --git a/Arithmetization/IDeltaZero/Exponential/Log.lean b/Arithmetization/IDeltaZero/Exponential/Log.lean
index 3a39edb..5ba281f 100644
--- a/Arithmetization/IDeltaZero/Exponential/Log.lean
+++ b/Arithmetization/IDeltaZero/Exponential/Log.lean
@@ -12,7 +12,7 @@ namespace Model
 
 section ISigma₀
 
-variable [𝐈𝚫₀.Mod M]
+variable [M ⊧ₘ* 𝐈𝚫₀]
 
 lemma log_exists_unique_pos {y : M} (hy : 0 < y) : ∃! x, x < y ∧ ∃ y' ≤ y, Exp x y' ∧ y < 2 * y' := by
   have : ∃ x < y, ∃ y' ≤ y, Exp x y' ∧ y < 2 * y' := by
@@ -70,7 +70,7 @@ lemma log_graph {x y : M} : x = log y ↔ (y = 0 → x = 0) ∧ (0 < y → x < y
 def logDef : Δ₀-Sentence 2 := ⟨“(#1 = 0 → #0 = 0) ∧ (0 < #1 → #0 < #1 ∧ ∃[#0 < #2 + 1] (!Exp.def [#1, #0] ∧ #2 < 2 * #0))”, by simp⟩
 
 lemma log_defined : Δ₀-Function₁ (log : M → M) via logDef := by
-  intro v; simp [logDef, log_graph, Exp.defined.pval, ←le_iff_lt_succ]
+  intro v; simp [logDef, log_graph, Exp.defined.pval, ←le_iff_lt_succ, numeral_eq_natCast]
 
 instance log_definable : DefinableFunction₁ ℒₒᵣ Σ 0 (log : M → M) := defined_to_with_param _ log_defined
 
@@ -408,7 +408,7 @@ lemma fbit_eq_zero_of_le {a i : M} (hi : ‖a‖ ≤ i) : fbit a i = 0 := by sim
 def fbitDef : Δ₀-Sentence 3 := ⟨“∃[#0 < #2 + 1] (!bexpDef [#0, #2, #3] ∧ ∃[#0 < #3 + 1] (!divDef [#0, #3, #1] ∧ !remDef [#2, #0, 2]))”, by simp⟩
 
 lemma fbit_defined : Δ₀-Function₂ (fbit : M → M → M) via fbitDef := by
-  intro v; simp [fbitDef, bexp_defined.pval, div_defined.pval, rem_defined.pval, ←le_iff_lt_succ, fbit]
+  intro v; simp [fbitDef, bexp_defined.pval, div_defined.pval, rem_defined.pval, ←le_iff_lt_succ, fbit, numeral_eq_natCast]
   constructor
   · intro h; exact ⟨bexp (v 1) (v 2), by simp, rfl, _, by simp, rfl, h⟩
   · rintro ⟨_, _, rfl, _, _, rfl, h⟩; exact h
@@ -437,7 +437,7 @@ end ISigma₀
 
 section ISigma₁
 
-variable [𝐈𝚺₁.Mod M]
+variable [M ⊧ₘ* 𝐈𝚺₁]
 
 @[simp] lemma log_exponential (a : M) : log (exp a) = a := (exp_exponential a).log_eq_of_exp
 
diff --git a/Arithmetization/IDeltaZero/Exponential/PPow2.lean b/Arithmetization/IDeltaZero/Exponential/PPow2.lean
index 8d80ab7..d90dbcb 100644
--- a/Arithmetization/IDeltaZero/Exponential/PPow2.lean
+++ b/Arithmetization/IDeltaZero/Exponential/PPow2.lean
@@ -12,7 +12,7 @@ namespace Model
 
 section ISigma₀
 
-variable [𝐈𝚫₀.Mod M]
+variable [M ⊧ₘ* 𝐈𝚫₀]
 
 def SPPow2 (m : M) : Prop := ¬LenBit 1 m ∧ LenBit 2 m ∧ ∀ i ≤ m, Pow2 i → 2 < i → (LenBit i m ↔ (√i)^2 = i ∧ LenBit (√i) m)
 
@@ -23,7 +23,8 @@ def sppow2Def : Δ₀-Sentence 1 :=
 
 lemma sppow2_defined : Δ₀-Predicate (SPPow2 : M → Prop) via sppow2Def := by
   intro v
-  simp [SPPow2, sppow2Def, Matrix.vecHead, Matrix.vecTail, lenbit_defined.pval, pow2_defined.pval, sqrt_defined.pval, ←le_iff_lt_succ, sq]
+  simp [SPPow2, sppow2Def, Matrix.vecHead, Matrix.vecTail, lenbit_defined.pval,
+    pow2_defined.pval, sqrt_defined.pval, ←le_iff_lt_succ, sq, numeral_eq_natCast]
   intro _ _; apply ball_congr; intro x _; apply imp_congr_right; intro _; apply imp_congr_right; intro _; apply iff_congr
   · simp
   · constructor
@@ -36,7 +37,8 @@ def ppow2Def : Δ₀-Sentence 1 :=
   ⟨“!pow2Def [#0] ∧ ∃[#0 < 2 * #1] (!sppow2Def [#0] ∧ !lenbitDef [#1, #0])”, by simp⟩
 
 lemma ppow2_defined : Δ₀-Predicate (PPow2 : M → Prop) via ppow2Def := by
-  intro v; simp[PPow2, ppow2Def, Matrix.vecHead, Matrix.vecTail, lenbit_defined.pval, pow2_defined.pval, sppow2_defined.pval]
+  intro v; simp[PPow2, ppow2Def, Matrix.vecHead, Matrix.vecTail,
+    lenbit_defined.pval, pow2_defined.pval, sppow2_defined.pval, numeral_eq_natCast]
 
 instance ppow2_definable : DefinablePred ℒₒᵣ Σ 0 (PPow2 : M → Prop) := defined_to_with_param₀ _ ppow2_defined
 
diff --git a/Arithmetization/IDeltaZero/Exponential/Pow2.lean b/Arithmetization/IDeltaZero/Exponential/Pow2.lean
index b723fff..65c6fd7 100644
--- a/Arithmetization/IDeltaZero/Exponential/Pow2.lean
+++ b/Arithmetization/IDeltaZero/Exponential/Pow2.lean
@@ -12,7 +12,7 @@ namespace Model
 
 section IOpen
 
-variable [𝐈open.Mod M]
+variable [M ⊧ₘ* 𝐈open]
 
 def Pow2 (a : M) : Prop := 0 < a ∧ ∀ r ≤ a, 1 < r → r ∣ a → 2 ∣ r
 
@@ -22,7 +22,7 @@ def pow2Def : Δ₀-Sentence 1 :=
 lemma pow2_defined : Δ₀-Predicate (Pow2 : M → Prop) via pow2Def := by
   intro v
   simp [Semiformula.eval_substs, Matrix.comp_vecCons', Matrix.vecHead, Matrix.constant_eq_singleton,
-    Pow2, pow2Def, le_iff_lt_succ, dvd_defined.pval]
+    Pow2, pow2Def, le_iff_lt_succ, dvd_defined.pval, numeral_eq_natCast]
 
 instance pow2_definable : DefinablePred ℒₒᵣ Σ 0 (Pow2 : M → Prop) := defined_to_with_param _ pow2_defined
 
@@ -114,7 +114,8 @@ def lenbitDef : Δ₀-Sentence 2 :=
   ⟨“∃[#0 < #2 + 1] (!divDef [#0, #2, #1] ∧ ¬!dvdDef [2, #0])”, by simp⟩
 
 lemma lenbit_defined : Δ₀-Relation (LenBit : M → M → Prop) via lenbitDef := by
-  intro v; simp[sqrt_graph, lenbitDef, Matrix.vecHead, Matrix.vecTail, div_defined.pval, dvd_defined.pval, LenBit, ←le_iff_lt_succ]
+  intro v; simp[sqrt_graph, lenbitDef, Matrix.vecHead, Matrix.vecTail,
+    div_defined.pval, dvd_defined.pval, LenBit, ←le_iff_lt_succ, numeral_eq_natCast]
   constructor
   · intro h; exact ⟨v 1 / v 0, by simp, rfl, h⟩
   · rintro ⟨z, hz, rfl, h⟩; exact h
@@ -193,7 +194,7 @@ end IOpen
 
 section ISigma₀
 
-variable [𝐈𝚫₀.Mod M]
+variable [M ⊧ₘ* 𝐈𝚫₀]
 
 namespace Pow2
 
diff --git a/Arithmetization/ISigmaOne/Bit.lean b/Arithmetization/ISigmaOne/Bit.lean
index 0b19bac..a6ab457 100644
--- a/Arithmetization/ISigmaOne/Bit.lean
+++ b/Arithmetization/ISigmaOne/Bit.lean
@@ -13,7 +13,7 @@ namespace Model
 
 section ISigma₁
 
-variable [𝐈𝚺₁.Mod M]
+variable [M ⊧ₘ* 𝐈𝚺₁]
 
 def Bit (i a : M) : Prop := LenBit (exp i) a
 
@@ -49,11 +49,11 @@ section
 
 variable {L : Language} [L.ORing] [Structure L M] [Structure.ORing L M] [Structure.Monotone L M]
 
-variable (Γ : Polarity) (ν : ℕ)
+variable (Γ : Polarity) (n : ℕ)
 
 @[definability] lemma Definable.ball_mem {P : (Fin k → M) → M → Prop} {f : (Fin k → M) → M}
-    (hf : Semipolynomial L Γ ν f) (h : Definable L Γ ν (fun w ↦ P (w ·.succ) (w 0))) :
-    Definable L Γ ν (fun v ↦ ∀ x ∈ f v, P v x) := by
+    (hf : Semipolynomial L Γ n f) (h : Definable L Γ n (fun w ↦ P (w ·.succ) (w 0))) :
+    Definable L Γ n (fun v ↦ ∀ x ∈ f v, P v x) := by
   rcases hf.bounded with ⟨bf, hbf⟩
   rcases hf.definable with ⟨f_graph, hf_graph⟩
   rcases h with ⟨p, hp⟩
@@ -65,8 +65,8 @@ variable (Γ : Polarity) (ν : ℕ)
         · rintro ⟨_, _, rfl, h⟩ x hx; exact h x (lt_of_mem hx) hx⟩
 
 @[definability] lemma Definable.bex_mem {P : (Fin k → M) → M → Prop} {f : (Fin k → M) → M}
-    (hf : Semipolynomial L Γ ν f) (h : Definable L Γ ν (fun w ↦ P (w ·.succ) (w 0))) :
-    Definable L Γ ν (fun v ↦ ∃ x ∈ f v, P v x) := by
+    (hf : Semipolynomial L Γ n f) (h : Definable L Γ n (fun w ↦ P (w ·.succ) (w 0))) :
+    Definable L Γ n (fun v ↦ ∃ x ∈ f v, P v x) := by
   rcases hf.bounded with ⟨bf, hbf⟩
   rcases hf.definable with ⟨f_graph, hf_graph⟩
   rcases h with ⟨p, hp⟩
@@ -203,63 +203,63 @@ end ISigma₁
 
 section
 
-variable {ν : ℕ} [Fact (1 ≤ ν)] [(𝐈𝐍𝐃Σ ν).Mod M]
+variable {n : ℕ} [Fact (1 ≤ n)] [M ⊧ₘ* 𝐈𝐍𝐃Σ n]
 
-theorem finset_comprehension {P : M → Prop} (hP : Γ(ν)-Predicate P) (n : M) :
-    haveI : 𝐈𝚺₁.Mod M := mod_iSigma_of_le (show 1 ≤ ν from Fact.out)
-    ∃ s < exp n, ∀ i < n, i ∈ s ↔ P i := by
-  haveI : 𝐈𝚺₁.Mod M := mod_iSigma_of_le (show 1 ≤ ν from Fact.out)
-  have : ∃ s < exp n, ∀ i < n, P i → i ∈ s :=
-    ⟨under n, pred_lt_self_of_pos (by simp), fun i hi _ ↦ by simpa [mem_under_iff] using hi⟩
+theorem finset_comprehension {P : M → Prop} (hP : Γ(n)-Predicate P) (a : M) :
+    haveI : M ⊧ₘ* 𝐈𝚺₁ := mod_iSigma_of_le (show 1 ≤ n from Fact.out)
+    ∃ s < exp a, ∀ i < a, i ∈ s ↔ P i := by
+  haveI : M ⊧ₘ* 𝐈𝚺₁ := mod_iSigma_of_le (show 1 ≤ n from Fact.out)
+  have : ∃ s < exp a, ∀ i < a, P i → i ∈ s :=
+    ⟨under a, pred_lt_self_of_pos (by simp), fun i hi _ ↦ by simpa [mem_under_iff] using hi⟩
   rcases this with ⟨s, hsn, hs⟩
-  have : (Γ.alt)(ν)-Predicate (fun s ↦ ∀ i < n, P i → i ∈ s) := by
+  have : (Γ.alt)(n)-Predicate (fun s ↦ ∀ i < a, P i → i ∈ s) := by
     apply Definable.ball_lt; simp; apply Definable.imp
     definability
     apply @Definable.of_sigma_zero M ℒₒᵣ _ _ _ _ mem_definable
-  have : ∃ t, (∀ i < n, P i → i ∈ t) ∧ ∀ t' < t, ∃ x, P x ∧ x < n ∧ x ∉ t' := by
-    simpa using least_number_h (L := ℒₒᵣ) Γ.alt ν this hs
+  have : ∃ t, (∀ i < a, P i → i ∈ t) ∧ ∀ t' < t, ∃ x, P x ∧ x < a ∧ x ∉ t' := by
+    simpa using least_number_h (L := ℒₒᵣ) Γ.alt n this hs
   rcases this with ⟨t, ht, t_minimal⟩
   have t_le_s : t ≤ s := not_lt.mp (by
     intro lt
     rcases t_minimal s lt with ⟨i, hi, hin, his⟩
     exact his (hs i hin hi))
-  have : ∀ i < n, i ∈ t → P i := by
+  have : ∀ i < a, i ∈ t → P i := by
     intro i _ hit
     by_contra Hi
-    have : ∃ j, P j ∧ j < n ∧ (j ∈ t → j = i) := by
+    have : ∃ j, P j ∧ j < a ∧ (j ∈ t → j = i) := by
       simpa [not_imp_not] using t_minimal (bitRemove i t) (bitRemove_lt_of_mem hit)
     rcases this with ⟨j, Hj, hjn, hm⟩
     rcases hm (ht j hjn Hj); contradiction
   exact ⟨t, lt_of_le_of_lt t_le_s hsn, fun i hi ↦ ⟨this i hi, ht i hi⟩⟩
 
-theorem finset_comprehension_exists_unique {P : M → Prop} (hP : Γ(ν)-Predicate P) (n : M) :
-    haveI : 𝐈𝚺₁.Mod M := mod_iSigma_of_le (show 1 ≤ ν from Fact.out)
-    ∃! s, s < exp n ∧ ∀ i < n, i ∈ s ↔ P i := by
-  haveI : 𝐈𝚺₁.Mod M := mod_iSigma_of_le (show 1 ≤ ν from Fact.out)
-  rcases finset_comprehension hP n with ⟨s, hs, Hs⟩
+theorem finset_comprehension_exists_unique {P : M → Prop} (hP : Γ(n)-Predicate P) (a : M) :
+    haveI : M ⊧ₘ* 𝐈𝚺₁ := mod_iSigma_of_le (show 1 ≤ n from Fact.out)
+    ∃! s, s < exp a ∧ ∀ i < a, i ∈ s ↔ P i := by
+  haveI : M ⊧ₘ* 𝐈𝚺₁ := mod_iSigma_of_le (show 1 ≤ n from Fact.out)
+  rcases finset_comprehension hP a with ⟨s, hs, Hs⟩
   exact ExistsUnique.intro s ⟨hs, Hs⟩ (by
     intro t ⟨ht, Ht⟩
     apply mem_ext
     intro i
     constructor
     · intro hi
-      have hin : i < n := exponential_monotone.mp (lt_of_le_of_lt (exp_le_of_mem hi) ht)
+      have hin : i < a := exponential_monotone.mp (lt_of_le_of_lt (exp_le_of_mem hi) ht)
       exact (Hs i hin).mpr ((Ht i hin).mp hi)
     · intro hi
-      have hin : i < n := exponential_monotone.mp (lt_of_le_of_lt (exp_le_of_mem hi) hs)
+      have hin : i < a := exponential_monotone.mp (lt_of_le_of_lt (exp_le_of_mem hi) hs)
       exact (Ht i hin).mpr ((Hs i hin).mp hi))
 
 end
 
 section ISigma₁
 
-variable [𝐈𝚺₁.Mod M]
+variable [M ⊧ₘ* 𝐈𝚺₁]
 
 instance : Fact (1 ≤ 1) := ⟨by rfl⟩
 
-theorem finset_comprehension₁ {P : M → Prop} (hP : Γ(1)-Predicate P) (n : M) :
-    ∃ s < exp n, ∀ i < n, i ∈ s ↔ P i :=
-  finset_comprehension hP n
+theorem finset_comprehension₁ {P : M → Prop} (hP : Γ(1)-Predicate P) (a : M) :
+    ∃ s < exp a, ∀ i < a, i ∈ s ↔ P i :=
+  finset_comprehension hP a
 
 /-
 lemma domain_exists_unique (s : M) :
diff --git a/Arithmetization/OmegaOne/Basic.lean b/Arithmetization/OmegaOne/Basic.lean
index 04fd061..af9392d 100644
--- a/Arithmetization/OmegaOne/Basic.lean
+++ b/Arithmetization/OmegaOne/Basic.lean
@@ -5,14 +5,14 @@ namespace LO.FirstOrder
 namespace Arith
 
 /-- ∀ x, ∃ y, 2^{|x|^2} = y-/
-def omegaSentence₁ : Sentence ℒₒᵣ := “∀ ∃ ∃[#0 < #2 + 1] (!Model.lengthDef [#0, #2] ∧ !Model.Exp.def [#0*#0, #1])”
+def omegaOneAxiom : Sentence ℒₒᵣ := “∀ ∃ ∃[#0 < #2 + 1] (!Model.lengthDef [#0, #2] ∧ !Model.Exp.def [#0*#0, #1])”
 
 inductive Theory.omega₁ : Theory ℒₒᵣ where
-  | omega : Theory.omega₁ omegaSentence₁
+  | omega : Theory.omega₁ omegaOneAxiom
 
 notation "𝛀₁" => Theory.omega₁
 
-@[simp] lemma omega₁.mem_iff {σ} : σ ∈ 𝛀₁ ↔ σ = omegaSentence₁ :=
+@[simp] lemma omega₁.mem_iff {σ} : σ ∈ 𝛀₁ ↔ σ = omegaOneAxiom :=
   ⟨by rintro ⟨⟩; rfl, by rintro rfl; exact Theory.omega₁.omega⟩
 
 noncomputable section
@@ -21,8 +21,8 @@ namespace Model
 
 variable {M : Type} [Zero M] [One M] [Add M] [Mul M] [LT M]
 
-lemma models_Omega₁_iff [𝐈𝚫₀.Mod M] : M ⊧ₘ omegaSentence₁ ↔ ∀ x : M, ∃ y, Exp (‖x‖^2) y := by
-  simp [models_def, omegaSentence₁, length_defined.pval, Exp.defined.pval, sq, ←le_iff_lt_succ]
+lemma models_Omega₁_iff [M ⊧ₘ* 𝐈𝚫₀] : M ⊧ₘ omegaOneAxiom ↔ ∀ x : M, ∃ y, Exp (‖x‖^2) y := by
+  simp [models_def, omegaOneAxiom, length_defined.pval, Exp.defined.pval, sq, ←le_iff_lt_succ]
   constructor
   · intro h x
     rcases h x with ⟨y, _, _, rfl, h⟩; exact ⟨y, h⟩
@@ -30,14 +30,14 @@ lemma models_Omega₁_iff [𝐈𝚫₀.Mod M] : M ⊧ₘ omegaSentence₁ ↔ 
     rcases h x with ⟨y, h⟩
     exact ⟨y, ‖x‖, by simp, rfl, h⟩
 
-lemma sigma₁_omega₁ [𝐈𝚺₁.Mod M] : M ⊧ₘ omegaSentence₁ := models_Omega₁_iff.mpr (fun x ↦ Exp.range_exists (‖x‖^2))
+lemma sigma₁_omega₁ [M ⊧ₘ* 𝐈𝚺₁] : M ⊧ₘ omegaOneAxiom := models_Omega₁_iff.mpr (fun x ↦ Exp.range_exists (‖x‖^2))
 
-instance [𝐈𝚺₁.Mod M] : 𝛀₁.Mod M := ⟨by intro _; simp; rintro rfl; exact sigma₁_omega₁⟩
+instance [M ⊧ₘ* 𝐈𝚺₁] : M ⊧ₘ* 𝛀₁ := ⟨by intro _; simp; rintro rfl; exact sigma₁_omega₁⟩
 
-variable [𝐈𝚫₀.Mod M] [𝛀₁.Mod M]
+variable [M ⊧ₘ* 𝐈𝚫₀] [M ⊧ₘ* 𝛀₁]
 
 lemma exists_exp_sq_length (x : M) : ∃ y, Exp (‖x‖^2) y :=
-  models_Omega₁_iff.mp (Theory.Mod.models M Theory.omega₁.omega) x
+  models_Omega₁_iff.mp (ModelsTheory.models M Theory.omega₁.omega) x
 
 lemma exists_unique_exp_sq_length (x : M) : ∃! y, Exp (‖x‖^2) y := by
   rcases exists_exp_sq_length x with ⟨y, h⟩
@@ -120,7 +120,6 @@ lemma hash_two_mul_le_sq_hash (a b : M) : a # (2 * b) ≤ (a # b) ^ 2 := by
   · simp [hash_two_mul a pos, sq]
     exact hash_monotone (by rfl) (pos_iff_one_le.mp pos)
 
-
 end Model
 
 end
diff --git a/Arithmetization/OmegaOne/Nuon.lean b/Arithmetization/OmegaOne/Nuon.lean
index fe9b925..0ad2322 100644
--- a/Arithmetization/OmegaOne/Nuon.lean
+++ b/Arithmetization/OmegaOne/Nuon.lean
@@ -8,7 +8,7 @@ noncomputable section
 
 namespace Model
 
-variable {M : Type} [Zero M] [One M] [Add M] [Mul M] [LT M] [𝐈𝚺₀.Mod M] [𝛀₁.Mod M]
+variable {M : Type} [Zero M] [One M] [Add M] [Mul M] [LT M] [M ⊧ₘ* 𝐈𝚺₀] [M ⊧ₘ* 𝛀₁]
 
 namespace Nuon
 
@@ -80,7 +80,7 @@ def extDef : Δ₀-Sentence 4 :=
 @[simp] lemma cons_app_nine {n : ℕ} (a : α) (s : Fin n.succ.succ.succ.succ.succ.succ.succ.succ.succ → α) : (a :> s) 9 = s 8 := rfl
 
 lemma ext_defined : Δ₀-Function₃ (ext : M → M → M → M) via extDef := by
-  intro v; simp [extDef, length_defined.pval, Exp.defined.pval, div_defined.pval, rem_defined.pval, lt_succ_iff_le, ext_graph]
+  intro v; simp [extDef, length_defined.pval, Exp.defined.pval, div_defined.pval, rem_defined.pval, lt_succ_iff_le, ext_graph, numeral_eq_natCast]
 
 instance ext_Definable : DefinableFunction₃ ℒₒᵣ Σ 0 (ext : M → M → M → M) := defined_to_with_param₀ _ ext_defined
 
@@ -493,7 +493,7 @@ def isSegmentDef : Δ₀-Sentence 5 :=
         #2 = #1 + #0)))”, by simp⟩
 
 lemma isSegmentDef_defined : Defined (M := M) (λ v ↦ IsSegment (v 0) (v 1) (v 2) (v 3) (v 4)) isSegmentDef.val := by
-  intro v; simp [IsSegment, isSegmentDef, ext_defined.pval, fbit_defined.pval, lt_succ_iff_le]
+  intro v; simp [IsSegment, isSegmentDef, ext_defined.pval, fbit_defined.pval, lt_succ_iff_le, numeral_eq_natCast]
   apply ball_congr; intro x _
   constructor
   · intro h; exact ⟨_, by simp, rfl, _, by simp, rfl, _, by simp, rfl, h⟩
@@ -562,7 +562,7 @@ def nuonAuxDef : Δ₀-Sentence 3 :=
 
 lemma nuonAux_defined : Δ₀-Relation₃ (NuonAux : M → M → M → Prop) via nuonAuxDef := by
   intro v; simp [NuonAux, polyU, polyI, polyL, nuonAuxDef,
-    length_defined.pval, sqrt_defined.pval, bexp_defined.pval, seriesSegmentDef_defined.pval, lt_succ_iff_le]
+    length_defined.pval, sqrt_defined.pval, bexp_defined.pval, seriesSegmentDef_defined.pval, lt_succ_iff_le, numeral_eq_natCast]
   rw [bex_eq_le_iff, bex_eq_le_iff, bex_eq_le_iff, bex_eq_le_iff]; simp
 
 instance nuonAux_definable : DefinableRel₃ ℒₒᵣ Σ 0 (NuonAux : M → M → M → Prop) := defined_to_with_param _ nuonAux_defined
diff --git a/Arithmetization/Vorspiel/Lemmata.lean b/Arithmetization/Vorspiel/Lemmata.lean
index 07f8437..55c3f49 100644
--- a/Arithmetization/Vorspiel/Lemmata.lean
+++ b/Arithmetization/Vorspiel/Lemmata.lean
@@ -76,7 +76,7 @@ namespace Arith
 
 noncomputable section
 
-variable {M : Type} [Zero M] [One M] [Add M] [Mul M] [LT M] [𝐏𝐀⁻.Mod M]
+variable {M : Type} [Zero M] [One M] [Add M] [Mul M] [LT M] [M ⊧ₘ* 𝐏𝐀⁻]
 
 namespace Model
 
diff --git a/Arithmetization/Vorspiel/Vorspiel.lean b/Arithmetization/Vorspiel/Vorspiel.lean
index f0826d3..5af9d23 100644
--- a/Arithmetization/Vorspiel/Vorspiel.lean
+++ b/Arithmetization/Vorspiel/Vorspiel.lean
@@ -3,6 +3,8 @@ import Logic.FirstOrder.Arith.EA.Basic
 
 instance [Zero α] : Nonempty α := ⟨0⟩
 
+notation "exp " x:90 => Exp.exp x
+
 namespace Matrix
 
 lemma forall_iff {n : ℕ} (p : (Fin (n + 1) → α) → Prop) :
@@ -99,8 +101,8 @@ variable [𝓑 : System F] {α : Type*} [𝓢 : Semantics F α] [Complete F]
 lemma provableTheory_iff : T ⊢*! U ↔ (∀ s, s ⊧* T → s ⊧* U) := by
   simp [System.provableTheory_iff, ←consequence_iff_provable]
   constructor
-  · intro h s hs f hf; exact h f hf hs
-  · intro h f hf s hs; exact h s hs hf
+  · intro h s hs; exact ⟨fun f hf ↦ h f hf hs⟩
+  · intro h f hf s hs; exact (h s hs).realize hf
 
 end Complete
 
@@ -108,50 +110,6 @@ end
 
 namespace FirstOrder
 
-namespace Semiterm
-
-@[simp] lemma bshift_positive (t : Semiterm L ξ n) : Positive (Rew.bShift t) := by
-  induction t <;> simp
-
-lemma bv_eq_empty_of_positive {t : Semiterm L ξ 1} (ht : t.Positive) : t.bv = ∅ :=
-  Finset.eq_empty_of_forall_not_mem <| by simp [Positive, Fin.eq_zero] at ht ⊢; assumption
-
-variable {M : Type*} {s : Structure L M}
-
-@[simp] lemma val_toS {e : Fin n → M} (t : Semiterm L (Fin n) 0) :
-    bVal s e (Rew.toS t) = val s ![] e t := by
-  simp[val_rew, Matrix.empty_eq]; congr
-
-@[simp] lemma val_toF {e : Fin n → M} (t : Semiterm L Empty n) :
-    val s ![] e (Rew.toF t) = bVal s e t := by
-  simp[val_rew, Matrix.empty_eq]; congr
-  funext i; simp; contradiction
-
-end Semiterm
-
-namespace Rew
-
-lemma substs_bv (t : Semiterm L ξ n) (v : Fin n → Semiterm L ξ m) :
-    (Rew.substs v t).bv = t.bv.biUnion (fun i ↦ (v i).bv) := by
-  induction t <;> simp [Rew.func, Semiterm.bv_func, Finset.biUnion_biUnion, *]
-
-@[simp] lemma substs_positive (t : Semiterm L ξ n) (v : Fin n → Semiterm L ξ (m + 1)) :
-    (Rew.substs v t).Positive ↔ ∀ i ∈ t.bv, (v i).Positive := by
-  simp [Semiterm.Positive, substs_bv]
-  exact ⟨fun H i hi x hx ↦ H x i hi hx, fun H x i hi hx ↦ H i hi x hx⟩
-
-lemma embSubsts_bv (t : Semiterm L Empty n) (v : Fin n → Semiterm L ξ m) :
-    (Rew.embSubsts v t).bv = t.bv.biUnion (fun i ↦ (v i).bv) := by
-  induction t <;> simp [Rew.func, Semiterm.bv_func, Finset.biUnion_biUnion, *]
-  · contradiction
-
-@[simp] lemma embSubsts_positive (t : Semiterm L Empty n) (v : Fin n → Semiterm L ξ (m + 1)) :
-    (Rew.embSubsts v t).Positive ↔ ∀ i ∈ t.bv, (v i).Positive := by
-  simp [Semiterm.Positive, embSubsts_bv]
-  exact ⟨fun H i hi x hx ↦ H x i hi hx, fun H x i hi hx ↦ H i hi x hx⟩
-
-end Rew
-
 namespace Arith
 
 attribute [simp] Semiformula.eval_substs Semiformula.eval_embSubsts
@@ -195,34 +153,16 @@ instance : ToString (Semiformula ℒₒᵣ μ n) := ⟨formulaToStr⟩
 
 end ToString
 
-namespace Hierarchy
-
-variable {L : Language} [L.LT]
-
-lemma of_zero {b b'} {s : ℕ} {p : Semiformula L μ n} (hp : Hierarchy b 0 p) : Hierarchy b' s p := by
-  rcases Nat.eq_or_lt_of_le (Nat.zero_le s) with (rfl | pos)
-  · exact zero_iff.mp hp
-  · exact strict_mono hp b' pos
-
-lemma iff_iff {p q : Semiformula L μ n} :
-    Hierarchy b s (p ⟷ q) ↔ (Hierarchy b s p ∧ Hierarchy b.alt s p ∧ Hierarchy b s q ∧ Hierarchy b.alt s q) := by
-  simp[Semiformula.iff_eq]; tauto
-
-@[simp] lemma iff_iff₀ {p q : Semiformula L μ n} :
-    Hierarchy b 0 (p ⟷ q) ↔ (Hierarchy b 0 p ∧ Hierarchy b 0 q) := by
-  simp[Semiformula.iff_eq]; tauto
-
-end Hierarchy
-
 section model
 
 variable {T : Theory ℒₒᵣ} [𝐄𝐪 ≾ T]
 
-variable (M : Type) [Zero M] [One M] [Add M] [Mul M] [LT M] [T.Mod M]
+variable (M : Type) [Zero M] [One M] [Add M] [Mul M] [LT M] [M ⊧ₘ* T]
 
 lemma oring_sound {σ : Sentence ℒₒᵣ} (h : T ⊢! σ) : M ⊧ₘ σ := consequence_iff'.mp (LO.Sound.sound! h) M
 
-instance (Γ s) [(𝐈𝐍𝐃Γ s).Mod M] : (Theory.indScheme ℒₒᵣ (Arith.Hierarchy Γ s)).Mod M := mod_indScheme_of_mod_indH (Γ := Γ) (ν := s)
+instance (Γ n) [M ⊧ₘ* 𝐈𝐍𝐃Γ n] :
+    M ⊧ₘ* Theory.indScheme ℒₒᵣ (Arith.Hierarchy Γ n) := models_indScheme_of_models_indH Γ n
 
 end model
 
@@ -296,24 +236,6 @@ lemma bexClosure_iff {b s n} {p : Semiformula L ξ n} {v : Fin n → Semiterm L
   refine Iff.trans (IH (p := “∃[#0 < !!([→ #0] (v 0))] !p”) (v := (v ·.succ)) (by intro; simp [hv])) ?_
   rw [bex_iff]; simp [Semiterm.bv_eq_empty_of_positive (hv 0)]
 
-@[simp] lemma matrix_conj_iff {b s n} {p : Fin m → Semiformula L ξ n} :
-    Hierarchy b s (Matrix.conj fun j ↦ p j) ↔ ∀ j, Hierarchy b s (p j) := by
-  cases m <;> simp
-
-lemma remove_forall {p : Semiformula L ξ (n + 1)} : Hierarchy b s (∀' p) → Hierarchy b s p := by
-  intro h; rcases h
-  case ball => simpa
-  case all => assumption
-  case pi h => exact h.accum _
-  case dummy_sigma h => exact h.accum _
-
-lemma remove_exists {p : Semiformula L ξ (n + 1)} : Hierarchy b s (∃' p) → Hierarchy b s p := by
-  intro h; rcases h
-  case bex => simpa
-  case ex => assumption
-  case sigma h => exact h.accum _
-  case dummy_pi h => exact h.accum _
-
 end Arith.Hierarchy
 
 end
diff --git a/README.md b/README.md
index bb2702b..2aacfcd 100644
--- a/README.md
+++ b/README.md
@@ -38,11 +38,11 @@ https://iehality.github.io/Arithmetization/
 - [Order induction](https://iehality.github.io/Arithmetization/Arithmetization/Basic/Ind.html#LO.FirstOrder.Arith.Model.order_induction_h)
   ```lean
   theorem LO.FirstOrder.Arith.Model.induction_h
-      {M : Type} [Zero M] [One M] [Add M] [Mul M] [LT M] [LO.FirstOrder.Theory.Mod M 𝐏𝐀⁻]
+      {M : Type} [Zero M] [One M] [Add M] [Mul M] [LT M] [LO.FirstOrder.ModelsTheory M 𝐏𝐀⁻]
       {L : LO.FirstOrder.Language} [LO.FirstOrder.Language.ORing L]
       [LO.FirstOrder.Structure L M] [LO.FirstOrder.Structure.ORing L M]
       (Γ : LO.Polarity) (s : ℕ)
-      [LO.FirstOrder.Theory.Mod M (LO.FirstOrder.Arith.Theory.indScheme L (LO.FirstOrder.Arith.Hierarchy Γ s))]
+      [LO.FirstOrder.ModelsTheory M (LO.FirstOrder.Arith.Theory.indScheme L (LO.FirstOrder.Arith.Hierarchy Γ s))]
       {P : M → Prop} (hP : LO.FirstOrder.Arith.Model.DefinablePred L Γ s P)
       (ind : ∀ (x : M), (∀ y < x, P y) → P x) (x : M) :
       P x
@@ -51,12 +51,12 @@ https://iehality.github.io/Arithmetization/
 - [Least number principle](https://iehality.github.io/Arithmetization/Arithmetization/Basic/Ind.html#LO.FirstOrder.Arith.Model.least_number_h)
   ```lean
   theorem LO.FirstOrder.Arith.Model.least_number_h
-      {M : Type} [Zero M] [One M] [Add M] [Mul M] [LT M] [LO.FirstOrder.Theory.Mod M 𝐏𝐀⁻]
+      {M : Type} [Zero M] [One M] [Add M] [Mul M] [LT M] [LO.FirstOrder.ModelsTheory M 𝐏𝐀⁻]
       {L : LO.FirstOrder.Language} [LO.FirstOrder.Language.ORing L]
       [LO.FirstOrder.Structure L M] [LO.FirstOrder.Structure.ORing L M]
       [LO.FirstOrder.Structure.Monotone L M]
       (Γ : LO.Polarity) (s : ℕ)
-      [LO.FirstOrder.Theory.Mod M (LO.FirstOrder.Arith.Theory.indScheme L (LO.FirstOrder.Arith.Hierarchy Γ s))]
+      [LO.FirstOrder.ModelsTheory M (LO.FirstOrder.Arith.Theory.indScheme L (LO.FirstOrder.Arith.Hierarchy Γ s))]
       {P : M → Prop} (hP : LO.FirstOrder.Arith.Model.DefinablePred L Γ s P)
       {x : M} (h : P x) :
       ∃ (y : M), P y ∧ ∀ z < y, ¬P z
@@ -73,7 +73,7 @@ https://iehality.github.io/Arithmetization/
   - [LO.FirstOrder.Arith.Model.Exp.defined](https://iehality.github.io/Arithmetization/Arithmetization/IDeltaZero/Exponential/Exp.html#LO.FirstOrder.Arith.Model.Exp.defined)
     ```lean
     theorem LO.FirstOrder.Arith.Model.Exp.defined
-        {M : Type} [Zero M] [One M] [Add M] [Mul M] [LT M] [LO.FirstOrder.Theory.Mod M 𝐈𝚫₀] :
+        {M : Type} [Zero M] [One M] [Add M] [Mul M] [LT M] [LO.FirstOrder.ModelsTheory M 𝐈𝚫₀] :
         Δ₀-Relation LO.FirstOrder.Arith.Model.Exp via LO.FirstOrder.Arith.Model.Exp.def
     ```
 
@@ -83,6 +83,6 @@ https://iehality.github.io/Arithmetization/
     ```lean
     theorem LO.FirstOrder.Arith.Model.nuon_defined
         {M : Type} [Zero M] [One M] [Add M] [Mul M] [LT M]
-        [LO.FirstOrder.Theory.Mod M 𝐈𝚫₀] [LO.FirstOrder.Theory.Mod M 𝛀₁] :
+        [LO.FirstOrder.ModelsTheory M 𝐈𝚫₀] [LO.FirstOrder.ModelsTheory M 𝛀₁] :
         Δ₀-Function₁ LO.FirstOrder.Arith.Model.nuon via LO.FirstOrder.Arith.Model.nuonDef
     ```
diff --git a/lake-manifest.json b/lake-manifest.json
index 10420e4..af69fb8 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -103,7 +103,7 @@
   {"url": "https://github.com/iehality/lean4-logic",
    "type": "git",
    "subDir": null,
-   "rev": "f541a5ecc63ad81771043542f1fadf6d505b7241",
+   "rev": "4a0fca57e396112c141055d61e181a96bc6f7c0a",
    "name": "logic",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,