refactor

Arithmetization.lean

@@ -3,7 +3,10 @@ import Arithmetization.Vorspiel.Graph
 import Arithmetization.Vorspiel.Lemmata
 
 import Arithmetization.Definability.Init
-import Arithmetization.Definability.Definability
+import Arithmetization.Definability.Hierarchy
+import Arithmetization.Definability.Boldface
+import Arithmetization.Definability.BoundedBoldface
+import Arithmetization.Definability.Absoluteness
 
 import Arithmetization.Basic.PeanoMinus
 import Arithmetization.Basic.Ind
@@ -41,7 +44,6 @@ import Arithmetization.ISigmaOne.Metamath.Coding
 
 import Arithmetization.ISigmaOne.Metamath.Theory.R
 import Arithmetization.ISigmaOne.Metamath.Theory.SigmaOneDefinable
-import Arithmetization.ISigmaOne.Metamath.Theory.Theory
 
 import Arithmetization.ISigmaOne.Metamath.DerivabilityConditions.D1
 import Arithmetization.ISigmaOne.Metamath.DerivabilityConditions.D3

Arithmetization/Basic/PeanoMinus.lean

@@ -6,51 +6,51 @@ open FirstOrder FirstOrder.Arith
 
 noncomputable section
 
-variable {M : Type*} [Zero M] [One M] [Add M] [Mul M] [LT M] [M ⊧ₘ* 𝐏𝐀⁻]
+variable {V : Type*} [ORingStruc V] [V ⊧ₘ* 𝐏𝐀⁻]
 
-variable {a b c : M}
+variable {a b c : V}
 
 section sub
 
-lemma sub_existsUnique (a b : M) : ∃! c, (a ≥ b → a = b + c) ∧ (a < b → c = 0) := by
+lemma sub_existsUnique (a b : V) : ∃! c, (a ≥ b → a = b + c) ∧ (a < b → c = 0) := by
   have : b ≤ a ∨ a < b := le_or_lt b a
   rcases this with (hxy | hxy) <;> simp [hxy]
   have : ∃ c, a = b + c := exists_add_of_le hxy
   rcases this with ⟨c, rfl⟩
   exact ExistsUnique.intro c rfl (fun a h => (add_left_cancel h).symm)
 
-def sub (a b : M) : M := Classical.choose! (sub_existsUnique a b)
+def sub (a b : V) : V := Classical.choose! (sub_existsUnique a b)
 
-instance : Sub M := ⟨sub⟩
+instance : Sub V := ⟨sub⟩
 
 lemma sub_spec_of_ge (h : a ≥ b) : a = b + (a - b) := (Classical.choose!_spec (sub_existsUnique a b)).1 h
 
 lemma sub_spec_of_lt (h : a < b) : a - b = 0 := (Classical.choose!_spec (sub_existsUnique a b)).2 h
 
 lemma sub_eq_iff : c = a - b ↔ ((a ≥ b → a = b + c) ∧ (a < b → c = 0)) := Classical.choose!_eq_iff (sub_existsUnique a b)
 
-@[simp] lemma sub_le_self (a b : M) : a - b ≤ a := by
+@[simp] lemma sub_le_self (a b : V) : a - b ≤ a := by
   have : b ≤ a ∨ a < b := le_or_lt b a
   rcases this with (hxy | hxy) <;> simp[hxy]
   · simpa [← sub_spec_of_ge hxy] using show a - b ≤ b + (a - b) from le_add_self
   · simp[sub_spec_of_lt hxy]
 
-open Definability
+open FirstOrder.Arith.HierarchySymbol.Boldface
 
-def _root_.LO.FirstOrder.Arith.subDef : 𝚺₀-Semisentence 3 :=
+def _root_.LO.FirstOrder.Arith.subDef : 𝚺₀.Semisentence 3 :=
   .mkSigma “z x y | (x ≥ y → x = y + z) ∧ (x < y → z = 0)” (by simp[Hierarchy.pi_zero_iff_sigma_zero])
 
-lemma sub_defined : 𝚺₀-Function₂ ((· - ·) : M → M → M) via subDef := by
+lemma sub_defined : 𝚺₀-Function₂ ((· - ·) : V → V → V) via subDef := by
   intro v; simp [FirstOrder.Arith.subDef, sub_eq_iff]
 
 @[simp] lemma sub_defined_iff (v) :
-    Semiformula.Evalbm M v subDef.val ↔ v 0 = v 1 - v 2 := sub_defined.df.iff v
+    Semiformula.Evalbm V v subDef.val ↔ v 0 = v 1 - v 2 := sub_defined.df.iff v
 
-instance sub_definable (Γ) : DefinableFunction₂ ℒₒᵣ Γ ((· - ·) : M → M → M) := Defined.to_definable₀ _ sub_defined
+instance sub_definable (ℌ : HierarchySymbol) : ℌ.BoldfaceFunction₂ ((· - ·) : V → V → V) := sub_defined.to_definable₀
 
-instance sub_polybounded : Bounded₂ ℒₒᵣ ((· - ·) : M → M → M) := ⟨#0, λ _ ↦ by simp⟩
+instance sub_polybounded : Bounded₂ ((· - ·) : V → V → V) := ⟨#0, λ _ ↦ by simp⟩
 
-@[simp] lemma sub_self (a : M) : a - a = 0 :=
+@[simp] lemma sub_self (a : V) : a - a = 0 :=
   add_right_eq_self.mp (sub_spec_of_ge (a := a) (b := a) (by rfl)).symm
 
 lemma sub_spec_of_le (h : a ≤ b) : a - b = 0 := by
@@ -65,9 +65,9 @@ lemma add_tsub_self_of_le (h : b ≤ a) : b + (a - b) = a := by symm; exact sub_
 
 @[simp] lemma add_sub_self' : (b + a) - b = a := by simp [add_comm]
 
-@[simp] lemma zero_sub (a : M) : 0 - a = 0 := sub_spec_of_le (by simp)
+@[simp] lemma zero_sub (a : V) : 0 - a = 0 := sub_spec_of_le (by simp)
 
-@[simp] lemma sub_zero (a : M) : a - 0 = a := by
+@[simp] lemma sub_zero (a : V) : a - 0 = a := by
   simpa using sub_add_self_of_le (show 0 ≤ a from zero_le a)
 
 lemma sub_remove_left (e : a = b + c) : a - c = b := by simp[e]
@@ -97,7 +97,7 @@ lemma sub_sub : a - b - c = a - (b + c) := by
 @[simp] lemma sub_eq_zero_iff_le : a - b = 0 ↔ a ≤ b :=
   not_iff_not.mp (by simp [←pos_iff_ne_zero])
 
-instance : OrderedSub M where
+instance : OrderedSub V where
   tsub_le_iff_right := by
     intro a b c
     by_cases h : b ≤ a
@@ -107,7 +107,7 @@ instance : OrderedSub M where
     · simp [sub_spec_of_lt (show a < b from by simpa using h)]
       exact le_trans (le_of_lt $ show a < b from by simpa using h) (by simp)
 
-lemma zero_or_succ (a : M) : a = 0 ∨ ∃ a', a = a' + 1 := by
+lemma zero_or_succ (a : V) : a = 0 ∨ ∃ a', a = a' + 1 := by
   rcases zero_le a with (rfl | pos)
   · simp
   · right; exact ⟨a - 1, by rw [sub_add_self_of_le]; exact pos_iff_one_le.mp pos⟩
@@ -128,14 +128,14 @@ lemma sub_mul (h : b ≤ a) : (a - b) * c = a * c - b * c := by
 
 lemma mul_sub (h : b ≤ a) : c * (a - b) = c * a - c * b := by simp [mul_comm c, sub_mul, h]
 
-lemma add_sub_of_le (h : c ≤ b) (a : M) : a + b - c = a + (b - c) := add_tsub_assoc_of_le h a
+lemma add_sub_of_le (h : c ≤ b) (a : V) : a + b - c = a + (b - c) := add_tsub_assoc_of_le h a
 
-lemma sub_succ_add_succ {x y : M} (h : y < x) (z) : x - (y + 1) + (z + 1) = x - y + z := calc
+lemma sub_succ_add_succ {x y : V} (h : y < x) (z) : x - (y + 1) + (z + 1) = x - y + z := calc
   x - (y + 1) + (z + 1) = x - (y + 1) + 1 + z := by simp [add_assoc, add_comm]
   _                     = x - y - 1 + 1 + z   := by simp [sub_sub]
   _                     = x - y + z           := by simp; rw [sub_add_self_of_le (one_le_of_zero_lt _ (pos_sub_iff_lt.mpr h))]
 
-lemma le_sub_one_of_lt {a b : M} (h : a < b) : a ≤ b - 1 := by
+lemma le_sub_one_of_lt {a b : V} (h : a < b) : a ≤ b - 1 := by
   have : 1 ≤ b := one_le_of_zero_lt _ (pos_of_gt h)
   simp [le_iff_lt_succ, sub_add_self_of_le this, h]
 
@@ -150,23 +150,23 @@ lemma le_mul_self_of_pos_left (hy : 0 < b) : a ≤ b * a := by
 lemma le_mul_self_of_pos_right (hy : 0 < b) : a ≤ a * b := by
   simpa [mul_comm a b] using le_mul_self_of_pos_left hy
 
-lemma dvd_iff_bounded {a b : M} : a ∣ b ↔ ∃ c ≤ b, b = a * c := by
+lemma dvd_iff_bounded {a b : V} : a ∣ b ↔ ∃ c ≤ b, b = a * c := by
   by_cases hx : a = 0
   · simp[hx]; rintro rfl; exact ⟨0, by simp⟩
   · constructor
     · rintro ⟨c, rfl⟩; exact ⟨c, le_mul_self_of_pos_left (pos_iff_ne_zero.mpr hx), rfl⟩
     · rintro ⟨c, hz, rfl⟩; exact dvd_mul_right a c
 
-def _root_.LO.FirstOrder.Arith.dvd : 𝚺₀-Semisentence 2 :=
+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 : M ↦ a ∣ b) via dvd :=
+lemma dvd_defined : 𝚺₀-Relation (fun a b : V ↦ a ∣ b) via dvd :=
   fun v ↦ by simp [dvd_iff_bounded, Matrix.vecHead, Matrix.vecTail, dvd]
 
 @[simp] lemma dvd_defined_iff (v) :
-    Semiformula.Evalbm M v dvd.val ↔ v 0 ∣ v 1 := dvd_defined.df.iff v
+    Semiformula.Evalbm V v dvd.val ↔ v 0 ∣ v 1 := dvd_defined.df.iff v
 
-instance dvd_definable (Γ) : DefinableRel ℒₒᵣ Γ ((· ∣ ·) : M → M → Prop) := Defined.to_definable₀ _ dvd_defined
+instance dvd_definable (ℌ : HierarchySymbol) : ℌ.BoldfaceRel ((· ∣ ·) : V → V → Prop) := dvd_defined.to_definable₀
 
 section
 
@@ -197,30 +197,30 @@ lemma dvd_antisymm : a ∣ b → b ∣ a → a = b := by
 
 lemma dvd_one_iff : a ∣ 1 ↔ a = 1 := ⟨by { intro hx; exact dvd_antisymm hx (by simp) }, by rintro rfl; simp⟩
 
-theorem units_eq_one (u : Mˣ) : u = 1 :=
+theorem units_eq_one (u : Vˣ) : u = 1 :=
   Units.ext <| dvd_one_iff.mp ⟨u.inv, u.val_inv.symm⟩
 
-@[simp] lemma unit_iff_eq_one {a : M} : IsUnit a ↔ a = 1 :=
+@[simp] lemma unit_iff_eq_one {a : V} : IsUnit a ↔ a = 1 :=
   ⟨by rintro ⟨u, rfl⟩; simp [units_eq_one u], by rintro rfl; simp⟩
 
 section Prime
 
-lemma eq_one_or_eq_of_dvd_of_prime {p a : M} (pp : Prime p) (hxp : a ∣ p) : a = 1 ∨ a = p := by
+lemma eq_one_or_eq_of_dvd_of_prime {p a : V} (pp : Prime p) (hxp : a ∣ p) : a = 1 ∨ a = p := by
   have : p ∣ a ∨ a ∣ 1 := pp.left_dvd_or_dvd_right_of_dvd_mul (show a ∣ p * 1 from by simpa using hxp)
   rcases this with (hx | hx)
   · right; exact dvd_antisymm hxp hx
   · left; exact dvd_one_iff.mp hx
 
 /-
-lemma irreducible_iff_bounded {a : M} : Irreducible a ↔ 1 < a ∧ ∀ b ≤ a, (b ∣ a → b = 1 ∨ b = a) := by
+lemma irreducible_iff_bounded {a : V} : Irreducible a ↔ 1 < a ∧ ∀ b ≤ a, (b ∣ a → b = 1 ∨ b = a) := by
   constructor
   · intro ha
     have : 1 < a := by
       by_contra A
       simp [Irreducible.ne_one ha, Irreducible.ne_zero ha, le_one_iff_eq_zero_or_one] at A
     exact ⟨this, by {  }⟩
 
-lemma prime_iff_bounded {a : M} : Prime a ↔ 1 < a ∧ ∀ b ≤ a, (b ∣ a → b = 1 ∨ b = a) := by
+lemma prime_iff_bounded {a : V} : Prime a ↔ 1 < a ∧ ∀ b ≤ a, (b ∣ a → b = 1 ∨ b = a) := by
   constructor
   · intro prim
     have : 1 < a := by
@@ -236,13 +236,13 @@ lemma prime_iff_bounded {a : M} : Prime a ↔ 1 < a ∧ ∀ b ≤ a, (b ∣ a 
       · intro b c h
 -/
 
-def IsPrime (a : M) : Prop := 1 < a ∧ ∀ b ≤ a, b ∣ a → b = 1 ∨ b = a
+def IsPrime (a : V) : Prop := 1 < a ∧ ∀ b ≤ a, b ∣ a → b = 1 ∨ b = a
 -- TODO: prove IsPrime a ↔ Prime a
 
-def _root_.LO.FirstOrder.Arith.isPrime : 𝚺₀-Semisentence 1 :=
+def _root_.LO.FirstOrder.Arith.isPrime : 𝚺₀.Semisentence 1 :=
   .mkSigma “x | 1 < x ∧ ∀ y <⁺ x, !dvd.val y x → y = 1 ∨ y = x” (by simp [Hierarchy.pi_zero_iff_sigma_zero])
 
-lemma isPrime_defined : 𝚺₀-Predicate (λ a : M ↦ IsPrime a) via isPrime := by
+lemma isPrime_defined : 𝚺₀-Predicate (λ a : V ↦ IsPrime a) via isPrime := by
   intro v
   simp [Semiformula.eval_substs, Matrix.comp_vecCons', Matrix.vecHead, Matrix.constant_eq_singleton,
     IsPrime, isPrime]
@@ -251,10 +251,10 @@ end Prime
 
 section min
 
-def _root_.LO.FirstOrder.Arith.min : 𝚺₀-Semisentence 3 :=
+def _root_.LO.FirstOrder.Arith.min : 𝚺₀.Semisentence 3 :=
   .mkSigma “z x y | (x ≤ y → z = x) ∧ (x ≥ y → z = y)” (by simp)
 
-lemma min_defined : 𝚺₀-Function₂ (min : M → M → M) via min := by
+lemma min_defined : 𝚺₀-Function₂ (min : V → V → V) via min := by
   intro v; simp [FirstOrder.Arith.min]
   rcases le_total (v 1) (v 2) with (h | h) <;> simp [h]
   · intro h₀₁ h₂₁
@@ -263,20 +263,20 @@ lemma min_defined : 𝚺₀-Function₂ (min : M → M → M) via min := by
     exact le_antisymm (by simpa [h₀₂] using h) (by simpa [h₀₂] using h₁₂)
 
 @[simp] lemma eval_minDef (v) :
-    Semiformula.Evalbm M v min.val ↔ v 0 = min (v 1) (v 2) := min_defined.df.iff v
+    Semiformula.Evalbm V v min.val ↔ v 0 = min (v 1) (v 2) := min_defined.df.iff v
 
-instance min_definable (Γ) : Γ-Function₂ (min : M → M → M) := Defined.to_definable₀ _ min_defined
+instance min_definable (ℌ) : ℌ-Function₂ (min : V → V → V) := HierarchySymbol.Defined.to_definable₀ min_defined
 
-instance min_polybounded : Bounded₂ ℒₒᵣ (min : M → M → M) := ⟨#0, λ _ ↦ by simp⟩
+instance min_polybounded : Bounded₂ (min : V → V → V) := ⟨#0, λ _ ↦ by simp⟩
 
 end min
 
 section max
 
-def _root_.LO.FirstOrder.Arith.max : 𝚺₀-Semisentence 3 :=
+def _root_.LO.FirstOrder.Arith.max : 𝚺₀.Semisentence 3 :=
   .mkSigma “z x y | (x ≥ y → z = x) ∧ (x ≤ y → z = y)” (by simp)
 
-lemma max_defined : 𝚺₀-Function₂ (max : M → M → M) via max := by
+lemma max_defined : 𝚺₀-Function₂ (max : V → V → V) via max := by
   intro v; simp [Arith.max]
   rcases le_total (v 1) (v 2) with (h | h) <;> simp [h]
   · intro h₀₂ h₂₁
@@ -285,11 +285,11 @@ lemma max_defined : 𝚺₀-Function₂ (max : M → M → M) via max := by
     exact le_antisymm (by simpa [h₀₁] using h₁₂) (by simpa [h₀₁] using h)
 
 @[simp] lemma eval_maxDef (v) :
-    Semiformula.Evalbm M v max.val ↔ v 0 = max (v 1) (v 2) := max_defined.df.iff v
+    Semiformula.Evalbm V v max.val ↔ v 0 = max (v 1) (v 2) := max_defined.df.iff v
 
-instance max_definable (Γ) : Γ-Function₂ (max : M → M → M) := Defined.to_definable₀ _ max_defined
+instance max_definable (Γ) : Γ-Function₂ (max : V → V → V) := HierarchySymbol.Defined.to_definable₀ max_defined
 
-instance max_polybounded : Bounded₂ ℒₒᵣ (max : M → M → M) := ⟨‘#0 + #1’, λ v ↦ by simp⟩
+instance max_polybounded : Bounded₂ (max : V → V → V) := ⟨‘#0 + #1’, λ v ↦ by simp⟩
 
 end max
 

Arithmetization/Definability/Absoluteness.lean

@@ -1,4 +1,4 @@
-import Arithmetization.Definability.Definability
+import Arithmetization.Definability.BoundedBoldface
 
 noncomputable section
 
@@ -10,50 +10,50 @@ lemma nat_modelsWithParam_iff_models_substs {v : Fin k → ℕ} {p : Semisentenc
     ℕ ⊧ₘ[v] p ↔ ℕ ⊧ₘ (Rew.substs (fun i ↦ Semiterm.Operator.numeral ℒₒᵣ (v i)) |>.hom p) := by
   simp [models_iff]
 
-variable (M : Type*) [Zero M] [One M] [Add M] [Mul M] [LT M] [M ⊧ₘ* 𝐏𝐀⁻]
+variable (M : Type*) [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻]
 
 lemma modelsWithParam_iff_models_substs {v : Fin k → ℕ} {p : Semisentence ℒₒᵣ k} :
     M ⊧ₘ[fun i ↦ v i] p ↔ M ⊧ₘ (Rew.substs (fun i ↦ Semiterm.Operator.numeral ℒₒᵣ (v i)) |>.hom p) := by
   simp [models_iff, numeral_eq_natCast]
 
-lemma shigmaZero_absolute {k} (p : 𝚺₀-Semisentence k) (v : Fin k → ℕ) :
+lemma shigmaZero_absolute {k} (p : 𝚺₀.Semisentence k) (v : Fin k → ℕ) :
     ℕ ⊧ₘ[v] p.val ↔ M ⊧ₘ[fun i ↦ (v i)] p.val :=
   ⟨by simp [nat_modelsWithParam_iff_models_substs, modelsWithParam_iff_models_substs]; exact nat_extention_sigmaOne M (by simp),
    by simp [nat_modelsWithParam_iff_models_substs, modelsWithParam_iff_models_substs]; exact nat_extention_piOne M (by simp)⟩
 
-lemma Defined.shigmaZero_absolute {k} {R : (Fin k → ℕ) → Prop} {R' : (Fin k → M) → 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 → M) → Prop} {p : 𝚺₀.Semisentence k}
+    (hR : 𝚺₀.Defined R p) (hR' : 𝚺₀.Defined R' p) (v : Fin k → ℕ) :
     R v ↔ R' (fun i ↦ (v i : M)) := by
   simpa [hR.iff, hR'.iff] using Arith.shigmaZero_absolute M p v
 
-lemma DefinedFunction.shigmaZero_absolute_func {k} {f : (Fin k → ℕ) → ℕ} {f' : (Fin k → M) → M} {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 → M) → M} {p : 𝚺₀.Semisentence (k + 1)}
+    (hf : 𝚺₀.DefinedFunction f p) (hf' : 𝚺₀.DefinedFunction f' p) (v : Fin k → ℕ) :
     (f v : M) = f' (fun i ↦ (v i)) := by
   simpa using Defined.shigmaZero_absolute M hf hf' (f v :> v)
 
-lemma sigmaOne_upward_absolute {k} (p : 𝚺₁-Semisentence k) (v : Fin k → ℕ) :
+lemma sigmaOne_upward_absolute {k} (p : 𝚺₁.Semisentence k) (v : Fin k → ℕ) :
     ℕ ⊧ₘ[v] p.val → M ⊧ₘ[fun i ↦ (v i)] p.val := by
   simp [nat_modelsWithParam_iff_models_substs, modelsWithParam_iff_models_substs]
   exact nat_extention_sigmaOne M (by simp)
 
-lemma piOne_downward_absolute {k} (p : 𝚷₁-Semisentence k) (v : Fin k → ℕ) :
+lemma piOne_downward_absolute {k} (p : 𝚷₁.Semisentence k) (v : Fin k → ℕ) :
     M ⊧ₘ[fun i ↦ (v i)] p.val → ℕ ⊧ₘ[v] p.val := by
   simp [nat_modelsWithParam_iff_models_substs, modelsWithParam_iff_models_substs]
   exact nat_extention_piOne M (by simp)
 
-lemma deltaOne_absolute {k} (p : 𝚫₁-Semisentence k)
+lemma deltaOne_absolute {k} (p : 𝚫₁.Semisentence k)
     (properNat : p.ProperOn ℕ) (proper : p.ProperOn M) (v : Fin k → ℕ) :
     ℕ ⊧ₘ[v] p.val ↔ M ⊧ₘ[fun i ↦ (v i)] p.val :=
-  ⟨by simpa [HSemiformula.val_sigma] using sigmaOne_upward_absolute M p.sigma v,
+  ⟨by simpa [HierarchySymbol.Semiformula.val_sigma] using sigmaOne_upward_absolute M p.sigma v,
    by simpa [proper.iff', properNat.iff'] using piOne_downward_absolute M p.pi v⟩
 
-lemma Defined.shigmaOne_absolute {k} {R : (Fin k → ℕ) → Prop} {R' : (Fin k → M) → 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 → M) → Prop} {p : 𝚫₁.Semisentence k}
+    (hR : 𝚫₁.Defined R p) (hR' : 𝚫₁.Defined R' p) (v : Fin k → ℕ) :
     R v ↔ R' (fun i ↦ (v i : M)) := by
   simpa [hR.df.iff, hR'.df.iff] using deltaOne_absolute M p hR.proper hR'.proper v
 
-lemma DefinedFunction.shigmaOne_absolute_func {k} {f : (Fin k → ℕ) → ℕ} {f' : (Fin k → M) → M} {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 → M) → M} {p : 𝚺₁.Semisentence (k + 1)}
+    (hf : 𝚺₁.DefinedFunction f p) (hf' : 𝚺₁.DefinedFunction f' p) (v : Fin k → ℕ) :
     (f v : M) = f' (fun i ↦ (v i)) := by
   simpa using Defined.shigmaOne_absolute M hf.graph_delta hf'.graph_delta (f v :> v)