Merge pull request #9 from FormalizedFormalLogic/update

update Foundation @ "4887553585220c4681616d542cfdf1275b927d0f"

Arithmetization/Basic/IOpen.lean

@@ -20,9 +20,11 @@ lemma open_induction {P : V → Prop}
   induction (C := Semiformula.Open)
     (by rcases hP with ⟨p, hp, hhp⟩
         haveI : Inhabited V := Classical.inhabited_of_nonempty'
-        exact ⟨p.fvEnumInv, (Rew.rewriteMap p.fvEnum).hom p, by simp[hp],
+        exact ⟨p.fvarEnumInv, Rew.rewriteMap p.fvarEnum ▹ p, by simp[hp],
           by  intro x; simp [Semiformula.eval_rewriteMap, hhp]
-              exact Semiformula.eval_iff_of_funEqOn p (by intro z hz; simp [Semiformula.fvEnumInv_fvEnum hz])⟩) zero succ
+              exact Semiformula.eval_iff_of_funEqOn p (by
+                intro z hz
+                simp [Semiformula.fvarEnumInv_fvarEnum (Semiformula.mem_fvarList_iff_fvar?.mpr hz)])⟩) zero succ
 
 lemma open_leastNumber {P : V → Prop}
     (hP : ∃ p : Semiformula ℒₒᵣ V 1, p.Open ∧ ∀ x, P x ↔ Semiformula.Evalm V ![x] id p)
@@ -601,7 +603,7 @@ lemma pi₁_defined : 𝚺₀-Function₁ (pi₁ : V → V) via pi₁Def := by
   intro v; simp [pi₁Def]
   constructor
   · intro h; exact ⟨π₂ v 1, by simp [←le_iff_lt_succ],  by simp [h]⟩
-  · rintro ⟨a, _, e⟩; simp [e]
+  · rintro ⟨a, _, e⟩; simp [show v 1 = ⟪v 0, a⟫ from e]
 
 @[simp] lemma pi₁_defined_iff (v) :
     Semiformula.Evalbm V v pi₁Def.val ↔ v 0 = π₁ (v 1) := pi₁_defined.df.iff v
@@ -612,7 +614,7 @@ lemma pi₂_defined : 𝚺₀-Function₁ (pi₂ : V → V) via pi₂Def := by
   intro v; simp [pi₂Def]
   constructor
   · intro h; exact ⟨π₁ v 1, by simp [←le_iff_lt_succ], by simp [h]⟩
-  · rintro ⟨a, _, e⟩; simp [e]
+  · rintro ⟨a, _, e⟩; simp [show v 1 = ⟪a, v 0⟫ from e]
 
 @[simp] lemma pi₂_defined_iff (v) :
     Semiformula.Evalbm V v pi₂Def.val ↔ v 0 = π₂ (v 1) := pi₂_defined.df.iff v
@@ -680,8 +682,24 @@ def _root_.LO.FirstOrder.Arith.pair₅Def : 𝚺₀.Semisentence 6 :=
 def _root_.LO.FirstOrder.Arith.pair₆Def : 𝚺₀.Semisentence 7 :=
   .mkSigma “p a b c d e f. ∃ bcdef <⁺ p, !pair₅Def bcdef b c d e f ∧ !pairDef p a bcdef” (by simp)
 
+theorem fegergreg (v : Fin 4 → ℕ) : v (0 : Fin (Nat.succ 1)).succ.succ = v 2 := by { simp only [Nat.succ_eq_add_one,
+  Nat.reduceAdd, Fin.isValue, Fin.succ_zero_eq_one, Fin.succ_one_eq_two] }
+
+axiom P : Fin 3 → Prop
+
+theorem fin4 {n} : (2 : Fin (n + 3)).succ = 3 := rfl
+
+@[simp] theorem Fin.succ_zero_eq_one'' {n} : (0 : Fin (n + 1)).succ = 1 := rfl
+
+@[simp] theorem Fin.succ_two_eq_three {n} : (2 : Fin (n + 3)).succ = 3 := rfl
+
+example (v : Fin 4 → ℕ) : v (2 : Fin 3).succ = v 3 := by { simp [fin4] }
+
+theorem ss (v : Fin 4 → ℕ) : v (Fin.succ (0 : Fin (Nat.succ 1))).succ = v 2 := by { simp [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, Fin.succ_zero_eq_one, Fin.succ_one_eq_two] }
+
 lemma pair₃_defined : 𝚺₀-Function₃ ((⟪·, ·, ·⟫) : V → V → V → V) via pair₃Def := by
-  intro v; simp [pair₃Def]; rintro h; simp [h]
+  intro v; simp [pair₃Def]
+  rintro h; simp [h]
 
 @[simp] lemma eval_pair₃Def (v) :
     Semiformula.Evalbm V v pair₃Def.val ↔ v 0 = ⟪v 1, v 2, v 3⟫ := pair₃_defined.df.iff v

Arithmetization/Basic/Ind.lean

@@ -6,16 +6,16 @@ open FirstOrder.Theory
 
 variable {C C' : Semiformula ℒₒᵣ ℕ 1 → Prop}
 
-lemma mem_indScheme_of_mem {p : Semiformula ℒₒᵣ ℕ 1} (hp : C p) :
-    succInd p ∈ indScheme ℒₒᵣ C := by
-  simp [indScheme]; exact ⟨p, hp, rfl⟩
+lemma mem_indScheme_of_mem {φ : Semiformula ℒₒᵣ ℕ 1} (hp : C φ) :
+    succInd φ ∈ indScheme ℒₒᵣ C := by
+  simp [indScheme]; exact ⟨φ, hp, rfl⟩
 
-lemma mem_iOpen_of_qfree {p : Semiformula ℒₒᵣ ℕ 1} (hp : p.Open) :
-    succInd p ∈ indScheme ℒₒᵣ Semiformula.Open := by
-  exact ⟨p, hp, rfl⟩
+lemma mem_iOpen_of_qfree {φ : Semiformula ℒₒᵣ ℕ 1} (hp : φ.Open) :
+    succInd φ ∈ indScheme ℒₒᵣ Semiformula.Open := by
+  exact ⟨φ, hp, rfl⟩
 
-lemma indScheme_subset (h : ∀ {p : Semiformula ℒₒᵣ ℕ 1},  C p → C' p) : indScheme ℒₒᵣ C ⊆ indScheme ℒₒᵣ C' := by
-  intro _; simp [indScheme]; rintro p hp rfl; exact ⟨p, h hp, rfl⟩
+lemma indScheme_subset (h : ∀ {φ : Semiformula ℒₒᵣ ℕ 1},  C φ → C' φ) : indScheme ℒₒᵣ C ⊆ indScheme ℒₒᵣ C' := by
+  intro _; simp [indScheme]; rintro φ hp rfl; exact ⟨φ, h hp, rfl⟩
 
 lemma iSigma_subset_mono {s₁ s₂} (h : s₁ ≤ s₂) : 𝐈𝚺 s₁ ⊆ 𝐈𝚺 s₂ :=
   Set.union_subset_union_right _ (indScheme_subset (fun H ↦ H.mono h))
@@ -36,21 +36,21 @@ section IndScheme
 
 variable {C : Semiformula ℒₒᵣ ℕ 1 → Prop} [V ⊧ₘ* Theory.indScheme ℒₒᵣ C]
 
-private lemma induction_eval {p : Semiformula ℒₒᵣ ℕ 1} (hp : C p) (v) :
-    Semiformula.Evalm V ![0] v p →
-    (∀ x, Semiformula.Evalm V ![x] v p → Semiformula.Evalm V ![x + 1] v p) →
-    ∀ x, Semiformula.Evalm V ![x] v p := by
-  have : V ⊧ₘ succInd p :=
+private lemma induction_eval {φ : Semiformula ℒₒᵣ ℕ 1} (hp : C φ) (v) :
+    Semiformula.Evalm V ![0] v φ →
+    (∀ x, Semiformula.Evalm V ![x] v φ → Semiformula.Evalm V ![x + 1] v φ) →
+    ∀ x, Semiformula.Evalm V ![x] v φ := by
+  have : V ⊧ₘ succInd φ :=
     ModelsTheory.models (T := Theory.indScheme _ C) V (by simpa using 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
 
 @[elab_as_elim]
 lemma induction {P : V → Prop}
-    (hP : ∃ e : ℕ → V, ∃ p : Semiformula ℒₒᵣ ℕ 1, C p ∧ ∀ x, P x ↔ Semiformula.Evalm V ![x] e p) :
+    (hP : ∃ e : ℕ → V, ∃ φ : Semiformula ℒₒᵣ ℕ 1, C φ ∧ ∀ x, P x ↔ Semiformula.Evalm V ![x] e φ) :
     P 0 → (∀ x, P x → P (x + 1)) → ∀ x, P x := by
-  rcases hP with ⟨e, p, Cp, hp⟩; simpa [←hp] using induction_eval (V := V) Cp e
+  rcases hP with ⟨e, φ, Cp, hp⟩; simpa [←hp] using induction_eval (V := V) Cp e
 
 end IndScheme
 
@@ -63,12 +63,14 @@ variable (Γ : Polarity) (m : ℕ) [V ⊧ₘ* Theory.indScheme ℒₒᵣ (Arith.
 lemma induction_h {P : V → Prop} (hP : Γ-[m].BoldfacePred P)
     (zero : P 0) (succ : ∀ x, P x → P (x + 1)) : ∀ x, P x :=
   induction (P := P) (C := Hierarchy Γ m) (by
-    rcases hP with ⟨p, hp⟩
+    rcases hP with ⟨φ, hp⟩
     haveI : Inhabited V := Classical.inhabited_of_nonempty'
-    exact ⟨p.val.fvEnumInv, (Rew.rewriteMap p.val.fvEnum).hom p.val, by simp [hp],
+
+    exact ⟨φ.val.fvarEnumInv, (Rew.rewriteMap φ.val.fvarEnum) ▹ φ.val, by simp [hp],
       by  intro x; simp [Semiformula.eval_rewriteMap]
-          have : (Semiformula.Evalm V ![x] fun x => p.val.fvEnumInv (p.val.fvEnum x)) p.val ↔ (Semiformula.Evalm V ![x] id) p.val :=
-            Semiformula.eval_iff_of_funEqOn _ (by intro x hx; simp [Semiformula.fvEnumInv_fvEnum hx])
+          have : (Semiformula.Evalm V ![x] fun x ↦ φ.val.fvarEnumInv (φ.val.fvarEnum x)) φ.val ↔ (Semiformula.Evalm V ![x] id) φ.val :=
+            Semiformula.eval_iff_of_funEqOn _ (by
+              intro x hx; simp [Semiformula.fvarEnumInv_fvarEnum (Semiformula.mem_fvarList_iff_fvar?.mpr hx)])
           simp [this, hp.df.iff]⟩)
     zero succ
 
@@ -117,16 +119,16 @@ private lemma neg_induction_h {P : V → Prop} (hP : Γ-[m].BoldfacePred P)
 
 lemma models_indScheme_alt : V ⊧ₘ* Theory.indScheme ℒₒᵣ (Arith.Hierarchy Γ.alt m) := by
   simp [Theory.indH, Theory.indScheme]
-  rintro _ p hp rfl
+  rintro _ φ hp rfl
   simp [models_iff, succInd, Semiformula.eval_rew_q,
     Semiformula.eval_substs, Function.comp, Matrix.constant_eq_singleton]
   intro v H0 Hsucc x
-  have : Semiformula.Evalm V ![0] v p →
-    (∀ x, Semiformula.Evalm V ![x] v p → Semiformula.Evalm V ![x + 1] v p) →
-      ∀ x, Semiformula.Evalm V ![x] v p := by
+  have : Semiformula.Evalm V ![0] v φ →
+    (∀ x, Semiformula.Evalm V ![x] v φ → Semiformula.Evalm V ![x + 1] v φ) →
+      ∀ x, Semiformula.Evalm V ![x] v φ := by
     simpa using
-      neg_induction_h Γ m (P := λ x ↦ ¬Semiformula.Evalm V ![x] v p)
-        (.mkPolarity (∼(Rew.rewriteMap v).hom p) (by simpa using hp)
+      neg_induction_h Γ m (P := λ x ↦ ¬Semiformula.Evalm V ![x] v φ)
+        (.mkPolarity (∼(Rew.rewriteMap v ▹ φ)) (by simpa using hp)
         (by intro x; simp [←Matrix.constant_eq_singleton', Semiformula.eval_rewriteMap]))
   exact this H0 Hsucc x
 

Arithmetization/Basic/PeanoMinus.lean

@@ -161,7 +161,8 @@ def _root_.LO.FirstOrder.Arith.dvd : 𝚺₀.Semisentence 2 :=
   .mkSigma “x y. ∃ z <⁺ y, y = x * z” (by simp)
 
 lemma dvd_defined : 𝚺₀-Relation (fun a b : V ↦ a ∣ b) via dvd :=
-  fun v ↦ by simp [dvd_iff_bounded, Matrix.vecHead, Matrix.vecTail, dvd]
+  fun v ↦ by
+    simp [dvd_iff_bounded, Matrix.vecHead, Matrix.vecTail, dvd]
 
 @[simp] lemma dvd_defined_iff (v) :
     Semiformula.Evalbm V v dvd.val ↔ v 0 ∣ v 1 := dvd_defined.df.iff v

Arithmetization/Definability/Absoluteness.lean

@@ -4,54 +4,54 @@ namespace LO.FirstOrder.Arith
 
 open LO.Arith
 
-lemma nat_modelsWithParam_iff_models_substs {v : Fin k → ℕ} {p : Semisentence ℒₒᵣ k} :
-    ℕ ⊧/v p ↔ ℕ ⊧ₘ₀ (Rew.substs (fun i ↦ Semiterm.Operator.numeral ℒₒᵣ (v i)) |>.hom p) := by
+lemma nat_modelsWithParam_iff_models_substs {v : Fin k → ℕ} {φ : Semisentence ℒₒᵣ k} :
+    ℕ ⊧/v φ ↔ ℕ ⊧ₘ₀ (φ ⇜ (fun i ↦ Semiterm.Operator.numeral ℒₒᵣ (v i))) := by
   simp [models_iff]
 
 variable (V : Type*) [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻]
 
-lemma modelsWithParam_iff_models_substs {v : Fin k → ℕ} {p : Semisentence ℒₒᵣ k} :
-    V ⊧/(v ·) p ↔ V ⊧ₘ₀ (Rew.substs (fun i ↦ Semiterm.Operator.numeral ℒₒᵣ (v i)) |>.hom p) := by
+lemma modelsWithParam_iff_models_substs {v : Fin k → ℕ} {φ : Semisentence ℒₒᵣ k} :
+    V ⊧/(v ·) φ ↔ V ⊧ₘ₀ (φ ⇜ (fun i ↦ Semiterm.Operator.numeral ℒₒᵣ (v i))) := by
   simp [models_iff, numeral_eq_natCast]
 
-lemma shigmaZero_absolute {k} (p : 𝚺₀.Semisentence k) (v : Fin k → ℕ) :
-    ℕ ⊧/v p.val ↔ V ⊧/(v ·) p.val :=
+lemma shigmaZero_absolute {k} (φ : 𝚺₀.Semisentence k) (v : Fin k → ℕ) :
+    ℕ ⊧/v φ.val ↔ V ⊧/(v ·) φ.val :=
   ⟨by simp [nat_modelsWithParam_iff_models_substs, modelsWithParam_iff_models_substs]; exact nat_extention_sigmaOne V (by simp),
    by simp [nat_modelsWithParam_iff_models_substs, modelsWithParam_iff_models_substs]; exact nat_extention_piOne V (by simp)⟩
 
-lemma Defined.shigmaZero_absolute {k} {R : (Fin k → ℕ) → Prop} {R' : (Fin k → V) → Prop} {p : 𝚺₀.Semisentence k}
-    (hR : 𝚺₀.Defined R p) (hR' : 𝚺₀.Defined R' p) (v : Fin k → ℕ) :
+lemma Defined.shigmaZero_absolute {k} {R : (Fin k → ℕ) → Prop} {R' : (Fin k → V) → Prop} {φ : 𝚺₀.Semisentence k}
+    (hR : 𝚺₀.Defined R φ) (hR' : 𝚺₀.Defined R' φ) (v : Fin k → ℕ) :
     R v ↔ R' (fun i ↦ (v i : V)) := by
-  simpa [hR.iff, hR'.iff] using Arith.shigmaZero_absolute V p v
+  simpa [hR.iff, hR'.iff] using Arith.shigmaZero_absolute V φ v
 
-lemma DefinedFunction.shigmaZero_absolute_func {k} {f : (Fin k → ℕ) → ℕ} {f' : (Fin k → V) → V} {p : 𝚺₀.Semisentence (k + 1)}
-    (hf : 𝚺₀.DefinedFunction f p) (hf' : 𝚺₀.DefinedFunction f' p) (v : Fin k → ℕ) :
+lemma DefinedFunction.shigmaZero_absolute_func {k} {f : (Fin k → ℕ) → ℕ} {f' : (Fin k → V) → V} {φ : 𝚺₀.Semisentence (k + 1)}
+    (hf : 𝚺₀.DefinedFunction f φ) (hf' : 𝚺₀.DefinedFunction f' φ) (v : Fin k → ℕ) :
     (f v : V) = f' (fun i ↦ (v i)) := by
   simpa using Defined.shigmaZero_absolute V hf hf' (f v :> v)
 
-lemma sigmaOne_upward_absolute {k} (p : 𝚺₁.Semisentence k) (v : Fin k → ℕ) :
-    ℕ ⊧/v p.val → V ⊧/(v ·) p.val := by
+lemma sigmaOne_upward_absolute {k} (φ : 𝚺₁.Semisentence k) (v : Fin k → ℕ) :
+    ℕ ⊧/v φ.val → V ⊧/(v ·) φ.val := by
   simp [nat_modelsWithParam_iff_models_substs, modelsWithParam_iff_models_substs]
   exact nat_extention_sigmaOne V (by simp)
 
-lemma piOne_downward_absolute {k} (p : 𝚷₁.Semisentence k) (v : Fin k → ℕ) :
-    V ⊧/(v ·) p.val → ℕ ⊧/v p.val := by
+lemma piOne_downward_absolute {k} (φ : 𝚷₁.Semisentence k) (v : Fin k → ℕ) :
+    V ⊧/(v ·) φ.val → ℕ ⊧/v φ.val := by
   simp [nat_modelsWithParam_iff_models_substs, modelsWithParam_iff_models_substs]
   exact nat_extention_piOne V (by simp)
 
-lemma deltaOne_absolute {k} (p : 𝚫₁.Semisentence k)
-    (properNat : p.ProperOn ℕ) (proper : p.ProperOn V) (v : Fin k → ℕ) :
-    ℕ ⊧/v p.val ↔ V ⊧/(v ·) p.val :=
-  ⟨by simpa [HierarchySymbol.Semiformula.val_sigma] using sigmaOne_upward_absolute V p.sigma v,
-   by simpa [proper.iff', properNat.iff'] using piOne_downward_absolute V p.pi v⟩
+lemma deltaOne_absolute {k} (φ : 𝚫₁.Semisentence k)
+    (properNat : φ.ProperOn ℕ) (proper : φ.ProperOn V) (v : Fin k → ℕ) :
+    ℕ ⊧/v φ.val ↔ V ⊧/(v ·) φ.val :=
+  ⟨by simpa [HierarchySymbol.Semiformula.val_sigma] using sigmaOne_upward_absolute V φ.sigma v,
+   by simpa [proper.iff', properNat.iff'] using piOne_downward_absolute V φ.pi v⟩
 
-lemma Defined.shigmaOne_absolute {k} {R : (Fin k → ℕ) → Prop} {R' : (Fin k → V) → Prop} {p : 𝚫₁.Semisentence k}
-    (hR : 𝚫₁.Defined R p) (hR' : 𝚫₁.Defined R' p) (v : Fin k → ℕ) :
+lemma Defined.shigmaOne_absolute {k} {R : (Fin k → ℕ) → Prop} {R' : (Fin k → V) → Prop} {φ : 𝚫₁.Semisentence k}
+    (hR : 𝚫₁.Defined R φ) (hR' : 𝚫₁.Defined R' φ) (v : Fin k → ℕ) :
     R v ↔ R' (fun i ↦ (v i : V)) := by
-  simpa [hR.df.iff, hR'.df.iff] using deltaOne_absolute V p hR.proper hR'.proper v
+  simpa [hR.df.iff, hR'.df.iff] using deltaOne_absolute V φ hR.proper hR'.proper v
 
-lemma DefinedFunction.shigmaOne_absolute_func {k} {f : (Fin k → ℕ) → ℕ} {f' : (Fin k → V) → V} {p : 𝚺₁.Semisentence (k + 1)}
-    (hf : 𝚺₁.DefinedFunction f p) (hf' : 𝚺₁.DefinedFunction f' p) (v : Fin k → ℕ) :
+lemma DefinedFunction.shigmaOne_absolute_func {k} {f : (Fin k → ℕ) → ℕ} {f' : (Fin k → V) → V} {φ : 𝚺₁.Semisentence (k + 1)}
+    (hf : 𝚺₁.DefinedFunction f φ) (hf' : 𝚺₁.DefinedFunction f' φ) (v : Fin k → ℕ) :
     (f v : V) = f' (fun i ↦ (v i)) := by
   simpa using Defined.shigmaOne_absolute V hf.graph_delta hf'.graph_delta (f v :> v)
 
@@ -82,28 +82,28 @@ variable {T : Theory ℒₒᵣ} [𝐏𝐀⁻ ≼ T] [Sigma1Sound T]
 noncomputable instance : 𝐑₀ ≼ T := System.Subtheory.comp (𝓣 := 𝐏𝐀⁻) inferInstance inferInstance
 
 theorem sigma_one_completeness_iff_param {σ : Semisentence ℒₒᵣ n} (hσ : Hierarchy 𝚺 1 σ) {e : Fin n → ℕ} :
-    ℕ ⊧/e σ ↔ T ⊢!. (Rew.substs fun x ↦ Semiterm.Operator.numeral ℒₒᵣ (e x)).hom σ := Iff.trans
+    ℕ ⊧/e σ ↔ T ⊢!. (σ ⇜ fun x ↦ Semiterm.Operator.numeral ℒₒᵣ (e x)) := Iff.trans
   (by simp [models_iff, Semiformula.eval_substs])
   (sigma_one_completeness_iff (T := T) (by simp [hσ]))
 
 lemma models_iff_provable_of_Sigma0_param [V ⊧ₘ* T] {σ : Semisentence ℒₒᵣ n} (hσ : Hierarchy 𝚺 0 σ) {e : Fin n → ℕ} :
-    V ⊧/(e ·) σ ↔ T ⊢!. (Rew.substs fun x ↦ Semiterm.Operator.numeral ℒₒᵣ (e x)).hom σ := by
+    V ⊧/(e ·) σ ↔ T ⊢!. (σ ⇜ fun x ↦ Semiterm.Operator.numeral ℒₒᵣ (e x)) := by
   calc
     V ⊧/(e ·) σ ↔ ℕ ⊧/e σ        := by
       simp [models_iff_of_Sigma0 hσ]
-  _             ↔ T ⊢!. (Rew.substs fun x ↦ Semiterm.Operator.numeral ℒₒᵣ (e x)).hom σ := by
+  _             ↔ T ⊢!. (σ ⇜ fun x ↦ Semiterm.Operator.numeral ℒₒᵣ (e x)) := by
       apply sigma_one_completeness_iff_param (by simp [Hierarchy.of_zero hσ])
 
 lemma models_iff_provable_of_Delta1_param [V ⊧ₘ* T] {σ : 𝚫₁.Semisentence n} (hσ : σ.ProperOn ℕ) (hσV : σ.ProperOn V) {e : Fin n → ℕ} :
-    V ⊧/(e ·) σ.val ↔ T ⊢!. (Rew.substs fun x ↦ Semiterm.Operator.numeral ℒₒᵣ (e x)).hom σ := by
+    V ⊧/(e ·) σ.val ↔ T ⊢!. (σ ⇜ fun x ↦ Semiterm.Operator.numeral ℒₒᵣ (e x)) := by
   calc
     V ⊧/(e ·) σ.val ↔ ℕ ⊧/e σ.val        := by
       simp [models_iff_of_Delta1 hσ hσV]
   _                 ↔ ℕ ⊧/e σ.sigma.val  := by
       simp [HierarchySymbol.Semiformula.val_sigma]
-  _                 ↔ T ⊢!. (Rew.substs fun x ↦ Semiterm.Operator.numeral ℒₒᵣ (e x)).hom σ.sigma.val := by
+  _                 ↔ T ⊢!. (σ.sigma.val ⇜ fun x ↦ Semiterm.Operator.numeral ℒₒᵣ (e x)) := by
       apply sigma_one_completeness_iff_param (by simp)
-  _                 ↔ T ⊢!. (Rew.substs fun x ↦ Semiterm.Operator.numeral ℒₒᵣ (e x)).hom σ.val       := by
+  _                 ↔ T ⊢!. (σ.val ⇜ fun x ↦ Semiterm.Operator.numeral ℒₒᵣ (e x))       := by
       simp [HierarchySymbol.Semiformula.val_sigma]
 
 end Arith