diff --git a/LeanPool/PointwiseComposition/CategoricalRiceShapiro/Evaluator/HistoryEvaluation.lean b/LeanPool/PointwiseComposition/CategoricalRiceShapiro/Evaluator/HistoryEvaluation.lean
index 690e1374d1..b0c816c98c 100644
--- a/LeanPool/PointwiseComposition/CategoricalRiceShapiro/Evaluator/HistoryEvaluation.lean
+++ b/LeanPool/PointwiseComposition/CategoricalRiceShapiro/Evaluator/HistoryEvaluation.lean
@@ -126,6 +126,16 @@ private theorem definable_code_graph {m : ℕ} (A : Code m) :
   intro w
   simp
 
+/-- Reuse the graph substitution theorem without simplifying its graph formula. -/
+private theorem definable_code_graph_values {k n : ℕ} (A : Code k)
+    (terms : Fin (k + 1) → ArithmeticSemiterm M n)
+    (values : (Fin n → M) → Fin (k + 1) → M)
+    (hvalues : ∀ w, Semiterm.val w id ∘ terms = values w) :
+    Σ-[1].Definable (fun w => Semiformula.Evalb (values w) (code A)) := by
+  refine (definable_code_graph_arguments A terms).of_iff ?_
+  intro w
+  rw [hvalues w]
+
 /-!
 ### Reading a supplied length evaluation -/
 
@@ -305,50 +315,19 @@ private theorem definable_match (Pc : Code 3) (w₀ w₁ b H bound : M) :
   have hS :
     Σ-[1].Definable (fun w : Fin 3 → M => Semiformula.Evalb ![w 0, w 1, w₀, w₁] (code Pc)) :=
     by
-    refine
-      ((definable_code_graph (M := M) Pc).retractiont (f :=
-            ![(#0 : ArithmeticSemiterm M 3), #1, &w₀, &w₁])).of_iff
-        ?_
-    intro w
-    have he :
-      (fun j => Semiterm.val w id (![(#0 : ArithmeticSemiterm M 3), #1, &w₀, &w₁] j)) =
-        ![w 0, w 1, w₀, w₁] :=
-      by
+      refine definable_code_graph_values Pc
+        ![(#0 : ArithmeticSemiterm M 3), #1, &w₀, &w₁] _ ?_
+      intro w
       funext j
-      refine Fin.cases ?_ ?_ j
-      · simp
-      · intro j1
-        refine Fin.cases ?_ ?_ j1
-        · simp
-        · intro j2
-          refine Fin.cases ?_ ?_ j2
-          · simp
-          · intro j3
-            refine Fin.cases ?_ (fun j4 => Fin.elim0 j4) j3
-            simp
-    rw [he]
+      fin_cases j <;> rfl
   have hD :
     Σ-[1].Definable (fun w : Fin 3 → M => Semiformula.Evalb ![w 0, w 2, H] (code dropCore)) :=
     by
-    refine
-      ((definable_code_graph (M := M) dropCore).retractiont (f :=
-            ![(#0 : ArithmeticSemiterm M 3), #2, &H])).of_iff
-        ?_
-    intro w
-    have he :
-      (fun j => Semiterm.val w id (![(#0 : ArithmeticSemiterm M 3), #2, &H] j)) =
-        ![w 0, w 2, H] :=
-      by
+      refine definable_code_graph_values dropCore
+        ![(#0 : ArithmeticSemiterm M 3), #2, &H] _ ?_
+      intro w
       funext j
-      refine Fin.cases ?_ ?_ j
-      · simp
-      · intro j1
-        refine Fin.cases ?_ ?_ j1
-        · simp
-        · intro j2
-          refine Fin.cases ?_ (fun j3 => Fin.elim0 j3) j2
-          simp
-    rw [he]
+      fin_cases j <;> rfl
   have hbody :
     Σ-[1].Definable
       (fun w : Fin 3 → M =>
@@ -451,25 +430,11 @@ private theorem drop_prefix [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] (H bnd z : M)
   have hD :
     Σ-[1].Definable (fun w : Fin 3 → M => Semiformula.Evalb ![w 0, w 1, H] (code dropCore)) :=
     by
-    refine
-      ((definable_code_graph (M := M) dropCore).retractiont (f :=
-            ![(#0 : ArithmeticSemiterm M 3), #1, &H])).of_iff
-        ?_
-    intro w
-    have he :
-      (fun j => Semiterm.val w id (![(#0 : ArithmeticSemiterm M 3), #1, &H] j)) =
-        ![w 0, w 1, H] :=
-      by
+      refine definable_code_graph_values dropCore
+        ![(#0 : ArithmeticSemiterm M 3), #1, &H] _ ?_
+      intro w
       funext j
-      refine Fin.cases ?_ ?_ j
-      · simp
-      · intro j1
-        refine Fin.cases ?_ ?_ j1
-        · simp
-        · intro j2
-          refine Fin.cases ?_ (fun j3 => Fin.elim0 j3) j2
-          simp
-    rw [he]
+      fin_cases j <;> rfl
   have hdef :
     Σ-[1].DefinablePred
       (fun j : M =>
@@ -537,25 +502,11 @@ private theorem drops_zero_from [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] (H c bound : M)
       Σ-[1].Definable
         (fun w : Fin 1 → M => Semiformula.Evalb ![(0 : M), w 0, H] (code dropCore)) :=
       by
-      refine
-        ((definable_code_graph (M := M) dropCore).retractiont (f :=
-              ![&(0 : M), (#0 : ArithmeticSemiterm M 1), &H])).of_iff
-          ?_
-      intro w
-      have he :
-        (fun j => Semiterm.val w id (![&(0 : M), (#0 : ArithmeticSemiterm M 1), &H] j)) =
-          ![(0 : M), w 0, H] :=
-        by
+        refine definable_code_graph_values dropCore
+          ![&(0 : M), (#0 : ArithmeticSemiterm M 1), &H] _ ?_
+        intro w
         funext j
-        refine Fin.cases ?_ ?_ j
-        · simp
-        · intro j1
-          refine Fin.cases ?_ ?_ j1
-          · simp
-          · intro j2
-            refine Fin.cases ?_ (fun j3 => Fin.elim0 j3) j2
-            simp
-      rw [he]
+        fin_cases j <;> rfl
     exact
       HierarchySymbol.Definable.imp (by definability)
         (HierarchySymbol.Definable.imp (by definability) hD)
@@ -638,41 +589,21 @@ private theorem definable_bad :
     Σ-[1].Definable
       (fun w : Fin 3 → M => Semiformula.Evalb ![w 1, w 2] (code codeEvaluatorHistory)) :=
     by
-    refine
-      ((definable_code_graph (M := M) codeEvaluatorHistory).retractiont (f :=
-            ![(#1 : ArithmeticSemiterm M 3), #2])).of_iff
-        ?_
-    intro w
-    have he :
-      (fun j => Semiterm.val w id (![(#1 : ArithmeticSemiterm M 3), #2] j)) = ![w 1, w 2] :=
-      by
+      refine definable_code_graph_values codeEvaluatorHistory
+        ![(#1 : ArithmeticSemiterm M 3), #2] _ ?_
+      intro w
       funext j
-      refine Fin.cases ?_ ?_ j
-      · simp
-      · intro j1
-        refine Fin.cases ?_ (fun j2 => Fin.elim0 j2) j1
-        simp
-    rw [he]
+      fin_cases j <;> rfl
   have hL :
     Σ-[1].Definable
       (fun w : Fin 3 → M =>
         Semiformula.Evalb ![w 0, w 1] (code (codeListLength (Code.proj (0 : Fin 1))))) :=
     by
-    refine
-      ((definable_code_graph (M := M) (codeListLength (Code.proj (0 : Fin 1)))).retractiont
-            (f := ![(#0 : ArithmeticSemiterm M 3), #1])).of_iff
-        ?_
-    intro w
-    have he :
-      (fun j => Semiterm.val w id (![(#0 : ArithmeticSemiterm M 3), #1] j)) = ![w 0, w 1] :=
-      by
+      refine definable_code_graph_values (codeListLength (Code.proj (0 : Fin 1)))
+        ![(#0 : ArithmeticSemiterm M 3), #1] _ ?_
+      intro w
       funext j
-      refine Fin.cases ?_ ?_ j
-      · simp
-      · intro j1
-        refine Fin.cases ?_ (fun j2 => Fin.elim0 j2) j1
-        simp
-    rw [he]
+      fin_cases j <;> rfl
   exact
     HierarchySymbol.Definable.exs
       (HierarchySymbol.Definable.exs (hH.and (hL.and (by definability))))
@@ -1563,65 +1494,31 @@ private theorem getAt_descend [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] (m i z Hm : M)
     Σ-[1].Definable
       (fun w : Fin 5 → M => Semiformula.Evalb ![w 2, w 3] (code codeEvaluatorHistory)) :=
     by
-    refine
-      ((definable_code_graph (M := M) codeEvaluatorHistory).retractiont (f :=
-            ![(#2 : ArithmeticSemiterm M 5), #3])).of_iff
-        ?_
-    intro w
-    have he :
-      (fun j => Semiterm.val w id (![(#2 : ArithmeticSemiterm M 5), #3] j)) = ![w 2, w 3] :=
-      by
+      refine definable_code_graph_values codeEvaluatorHistory
+        ![(#2 : ArithmeticSemiterm M 5), #3] _ ?_
+      intro w
       funext j
-      refine Fin.cases ?_ ?_ j
-      · simp
-      · intro j1
-        refine Fin.cases ?_ (fun j2 => Fin.elim0 j2) j1
-        simp
-    rw [he]
+      fin_cases j <;> rfl
   have hDrop :
     Σ-[1].Definable (fun w : Fin 5 → M => Semiformula.Evalb ![w 1, i, w 2] (code dropCore)) :=
     by
-    refine
-      ((definable_code_graph (M := M) dropCore).retractiont (f :=
-            ![(#1 : ArithmeticSemiterm M 5), &i, #2])).of_iff
-        ?_
-    intro w
-    have he :
-      (fun j => Semiterm.val w id (![(#1 : ArithmeticSemiterm M 5), &i, #2] j)) =
-        ![w 1, i, w 2] :=
-      by
+      refine definable_code_graph_values dropCore
+        ![(#1 : ArithmeticSemiterm M 5), &i, #2] _ ?_
+      intro w
       funext j
-      refine Fin.cases ?_ ?_ j
-      · simp
-      · intro j1
-        refine Fin.cases ?_ ?_ j1
-        · simp
-        · intro j2
-          refine Fin.cases ?_ (fun j3 => Fin.elim0 j3) j2
-          simp
-    rw [he]
+      fin_cases j <;> rfl
   have hHead :
     Σ-[1].Definable
       (fun w : Fin 5 → M =>
         Semiformula.Evalb ![w 0, w 1]
           (code (codeUnpair₁ (codeSub (Code.proj (0 : Fin 1)) (codeConst 1))))) :=
     by
-    refine
-      ((definable_code_graph (M := M)
-                (codeUnpair₁ (codeSub (Code.proj (0 : Fin 1)) (codeConst 1)))).retractiont
-            (f := ![(#0 : ArithmeticSemiterm M 5), #1])).of_iff
-        ?_
-    intro w
-    have he :
-      (fun j => Semiterm.val w id (![(#0 : ArithmeticSemiterm M 5), #1] j)) = ![w 0, w 1] :=
-      by
+      refine definable_code_graph_values
+        (codeUnpair₁ (codeSub (Code.proj (0 : Fin 1)) (codeConst 1)))
+        ![(#0 : ArithmeticSemiterm M 5), #1] _ ?_
+      intro w
       funext j
-      refine Fin.cases ?_ ?_ j
-      · simp
-      · intro j1
-        refine Fin.cases ?_ (fun j2 => Fin.elim0 j2) j1
-        simp
-    rw [he]
+      fin_cases j <;> rfl
   have hdef :
     Σ-[1].DefinablePred
       (fun t : M =>
@@ -2136,65 +2033,31 @@ private theorem history_ascent_definable :
     Σ-[1].Definable
       (fun w : Fin 5 → M => Semiformula.Evalb ![w 2, w 3] (code codeEvaluatorHistory)) :=
     by
-    refine
-      ((definable_code_graph (M := M) codeEvaluatorHistory).retractiont (f :=
-            ![(#2 : ArithmeticSemiterm M 5), #3])).of_iff
-        ?_
-    intro w
-    have he :
-      (fun j => Semiterm.val w id (![(#2 : ArithmeticSemiterm M 5), #3] j)) = ![w 2, w 3] :=
-      by
+      refine definable_code_graph_values codeEvaluatorHistory
+        ![(#2 : ArithmeticSemiterm M 5), #3] _ ?_
+      intro w
       funext j
-      refine Fin.cases ?_ ?_ j
-      · simp
-      · intro j1
-        refine Fin.cases ?_ (fun j2 => Fin.elim0 j2) j1
-        simp
-    rw [he]
+      fin_cases j <;> rfl
   have hDrop :
     Σ-[1].Definable (fun w : Fin 5 → M => Semiformula.Evalb ![w 1, P, w 2] (code dropCore)) :=
     by
-    refine
-      ((definable_code_graph (M := M) dropCore).retractiont (f :=
-            ![(#1 : ArithmeticSemiterm M 5), &P, #2])).of_iff
-        ?_
-    intro w
-    have he :
-      (fun j => Semiterm.val w id (![(#1 : ArithmeticSemiterm M 5), &P, #2] j)) =
-        ![w 1, P, w 2] :=
-      by
+      refine definable_code_graph_values dropCore
+        ![(#1 : ArithmeticSemiterm M 5), &P, #2] _ ?_
+      intro w
       funext j
-      refine Fin.cases ?_ ?_ j
-      · simp
-      · intro j1
-        refine Fin.cases ?_ ?_ j1
-        · simp
-        · intro j2
-          refine Fin.cases ?_ (fun j3 => Fin.elim0 j3) j2
-          simp
-    rw [he]
+      fin_cases j <;> rfl
   have hHead :
     Σ-[1].Definable
       (fun w : Fin 5 → M =>
         Semiformula.Evalb ![w 0, w 1]
           (code (codeUnpair₁ (codeSub (Code.proj (0 : Fin 1)) (codeConst 1))))) :=
     by
-    refine
-      ((definable_code_graph (M := M)
-                (codeUnpair₁ (codeSub (Code.proj (0 : Fin 1)) (codeConst 1)))).retractiont
-            (f := ![(#0 : ArithmeticSemiterm M 5), #1])).of_iff
-        ?_
-    intro w
-    have he :
-      (fun j => Semiterm.val w id (![(#0 : ArithmeticSemiterm M 5), #1] j)) = ![w 0, w 1] :=
-      by
+      refine definable_code_graph_values
+        (codeUnpair₁ (codeSub (Code.proj (0 : Fin 1)) (codeConst 1)))
+        ![(#0 : ArithmeticSemiterm M 5), #1] _ ?_
+      intro w
       funext j
-      refine Fin.cases ?_ ?_ j
-      · simp
-      · intro j1
-        refine Fin.cases ?_ (fun j2 => Fin.elim0 j2) j1
-        simp
-    rw [he]
+      fin_cases j <;> rfl
   have hbody :
     Σ-[1].Definable
       (fun w : Fin 5 → M =>
diff --git a/LeanPool/PointwiseComposition/Foundation/FirstOrder/Arithmetic/Bootstrapping/Syntax/Formula/Basic.lean b/LeanPool/PointwiseComposition/Foundation/FirstOrder/Arithmetic/Bootstrapping/Syntax/Formula/Basic.lean
index 2f8507da30..5e9866ac5d 100644
--- a/LeanPool/PointwiseComposition/Foundation/FirstOrder/Arithmetic/Bootstrapping/Syntax/Formula/Basic.lean
+++ b/LeanPool/PointwiseComposition/Foundation/FirstOrder/Arithmetic/Bootstrapping/Syntax/Formula/Basic.lean
@@ -520,7 +520,7 @@ lemma pos {p : V} (h : IsUFormula L p) : 0 < p := by
   rcases h.case with
       (⟨_, _, _, _, _, _, rfl⟩ | ⟨_, _, _, _, _, _, rfl⟩ | ⟨_, rfl⟩ | ⟨_, rfl⟩ |
         ⟨_, _, _, _, _, rfl⟩ | ⟨_, _, _, _, _, rfl⟩ | ⟨_, _, _, rfl⟩ | ⟨_, _, _, rfl⟩) <;>
-    simp [qqRel, qqNRel, qqVerum, qqFalsum, qqAnd, qqOr, qqAll, qqExs]
+    exact lt_of_le_of_lt zero_le (lt_add_one _)
       --lemma IsSemiformula.pos {n p : V} (h : Semiformula L n p) : 0 < p := h.1.pos
 
 @[simp]
@@ -1382,19 +1382,27 @@ lemma uformula_result_induction {P : V → V → V → Prop} (hP : Σ₁-Relatio
   rcases hp.case with
     (⟨k, r, v, hkr, hv, rfl⟩ | ⟨k, r, v, hkr, hv, rfl⟩ | rfl | rfl | ⟨p₁, p₂, hp₁, hp₂, rfl⟩ |
       ⟨p₁, p₂, hp₁, hp₂, rfl⟩ | ⟨p₁, hp₁, rfl⟩ | ⟨p₁, hp₁, rfl⟩)
-  · simpa [hkr, hv] using hRel param k r v hkr hv
-  · simpa [hkr, hv] using hNRel param k r v hkr hv
-  · simpa using hverum param
-  · simpa using hfalsum param
-  · simpa [c.result_and hp₁ hp₂] using
+  · rw [c.result_rel hkr hv]
+    exact hRel param k r v hkr hv
+  · rw [c.result_nrel hkr hv]
+    exact hNRel param k r v hkr hv
+  · rw [c.result_verum]
+    exact hverum param
+  · rw [c.result_falsum]
+    exact hfalsum param
+  · rw [c.result_and hp₁ hp₂]
+    exact
       hand param p₁ p₂ hp₁ hp₂ (ih p₁ (by simp) param (by simp [f]) hp₁)
         (ih p₂ (by simp) param (by simp [f]) hp₂)
-  · simpa [c.result_or hp₁ hp₂] using
+  · rw [c.result_or hp₁ hp₂]
+    exact
       hor param p₁ p₂ hp₁ hp₂ (ih p₁ (by simp) param (by simp [f]) hp₁)
         (ih p₂ (by simp) param (by simp [f]) hp₂)
-  · simpa [c.result_all hp₁] using
+  · rw [c.result_all hp₁]
+    exact
       hall param p₁ hp₁ (ih p₁ (by simp) (c.allChanges param) (by simp [f]) hp₁)
-  · simpa [c.result_exs hp₁] using
+  · rw [c.result_exs hp₁]
+    exact
       hexs param p₁ hp₁ (ih p₁ (by simp) (c.exsChanges param) (by simp [f]) hp₁)
 
 end Construction
@@ -1876,20 +1884,28 @@ lemma semiformula_result_induction {P : V → V → V → V → Prop} (hP : Σ
   rcases IsSemiformula.case_iff.mp hp with
     (⟨k, R, v, hR, hv, rfl⟩ | ⟨k, R, v, hR, hv, rfl⟩ | rfl | rfl | ⟨p₁, p₂, h₁, h₂, rfl⟩ |
       ⟨p₁, p₂, h₁, h₂, rfl⟩ | ⟨p₁, h₁, rfl⟩ | ⟨p₁, h₁, rfl⟩)
-  · simpa [hR, hv.isUTerm] using hRel n param k R v hR hv
-  · simpa [hR, hv.isUTerm] using hNRel n param k R v hR hv
-  · simpa using hverum n param
-  · simpa using hfalsum n param
-  · simpa [h₁.isUFormula, h₂.isUFormula] using
+  · rw [c.result_rel hR hv.isUTerm]
+    exact hRel n param k R v hR hv
+  · rw [c.result_nrel hR hv.isUTerm]
+    exact hNRel n param k R v hR hv
+  · rw [c.result_verum]
+    exact hverum n param
+  · rw [c.result_falsum]
+    exact hfalsum n param
+  · rw [c.result_and h₁.isUFormula h₂.isUFormula]
+    exact
       hand n param p₁ p₂ h₁ h₂ (ih p₁ (by simp) param (by simp [f]) n (by simp [g]) h₁)
         (ih p₂ (by simp) param (by simp [f]) n (by simp [g]) h₂)
-  · simpa [h₁.isUFormula, h₂.isUFormula] using
+  · rw [c.result_or h₁.isUFormula h₂.isUFormula]
+    exact
       hor n param p₁ p₂ h₁ h₂ (ih p₁ (by simp) param (by simp [f]) n (by simp [g]) h₁)
         (ih p₂ (by simp) param (by simp [f]) n (by simp [g]) h₂)
-  · simpa [h₁.isUFormula] using
+  · rw [c.result_all h₁.isUFormula]
+    exact
       hall n param p₁ h₁
         (ih p₁ (by simp) (c.allChanges param) (by simp [f]) (n + 1) (by simp [g]) h₁)
-  · simpa [h₁.isUFormula] using
+  · rw [c.result_exs h₁.isUFormula]
+    exact
       hexs n param p₁ h₁
         (ih p₁ (by simp) (c.exsChanges param) (by simp [f]) (n + 1) (by simp [g]) h₁)
 
diff --git a/LeanPool/PointwiseComposition/Foundation/FirstOrder/Arithmetic/HFS/Vec.lean b/LeanPool/PointwiseComposition/Foundation/FirstOrder/Arithmetic/HFS/Vec.lean
index 3e03da9431..b2bdbb6f9f 100644
--- a/LeanPool/PointwiseComposition/Foundation/FirstOrder/Arithmetic/HFS/Vec.lean
+++ b/LeanPool/PointwiseComposition/Foundation/FirstOrder/Arithmetic/HFS/Vec.lean
@@ -1316,6 +1316,11 @@ def blueprint : VecRec.Blueprint 0
   nil := .mkSigma (“y. y = 0”)
   adjoin := .mkSigma (“y x xs ih. !insertDef y x ih”)
 
+section
+
+-- Avoid expanding encoded formulas while elaborating this construction.
+attribute [local irreducible] blueprint
+
 /-- The adjointruction construction in `FFL.FirstOrder.Arithmetic.VecToSet`. -/
 noncomputable def adjointruction : VecRec.Construction V blueprint
     where
@@ -1324,6 +1329,8 @@ noncomputable def adjointruction : VecRec.Construction V blueprint
   nil_defined := .mk fun v ↦ by simp [blueprint, emptyset_def]
   adjoin_defined := .mk fun v ↦ by simp [blueprint]
 
+end
+
 end VecToSet
 
 section vecToSet
diff --git a/LeanPool/PointwiseComposition/Foundation/FirstOrder/Arithmetic/PeanoMinus/Basic.lean b/LeanPool/PointwiseComposition/Foundation/FirstOrder/Arithmetic/PeanoMinus/Basic.lean
index 2fa4bba121..3cdd3959bc 100644
--- a/LeanPool/PointwiseComposition/Foundation/FirstOrder/Arithmetic/PeanoMinus/Basic.lean
+++ b/LeanPool/PointwiseComposition/Foundation/FirstOrder/Arithmetic/PeanoMinus/Basic.lean
@@ -239,16 +239,19 @@ lemma le_def {x y : M} : x ≤ y ↔ x = y ∨ x < y :=
 variable [M↓[ℒₒᵣ] ⊧* 𝐏𝐀⁻]
 
 protected lemma add_zero' : ∀ x : M, x + 0 = x := by
-  simpa [models_iff] using Theory.models M _ PeanoMinus.addZero
+  exact models_iff.mp (Theory.models M _ PeanoMinus.addZero)
 
 protected lemma add_assoc : ∀ x y z : M, (x + y) + z = x + (y + z) := by
-  simpa [models_iff] using Theory.models M _ PeanoMinus.addAssoc
+  exact models_iff.mp (Theory.models M _ PeanoMinus.addAssoc)
 
 protected lemma add_comm : ∀ x y : M, x + y = y + x := by
-  simpa [models_iff] using Theory.models M _ PeanoMinus.addComm
+  exact models_iff.mp (Theory.models M _ PeanoMinus.addComm)
 
 lemma add_eq_of_lt : ∀ x y : M, x < y → ∃ z, x + z = y := by
-  simpa [models_iff] using Theory.models M _ PeanoMinus.addEqOfLt
+  have h := Theory.models M _ PeanoMinus.addEqOfLt
+  simp only [models_iff, Semiformula.eval_all, LogicalConnective.HomClass.map_imply,
+    LogicalConnective.Prop.arrow_eq, Semiformula.eval_ex] at h
+  exact h
 
 @[simp]
 protected lemma zero_le : ∀ x : M, 0 ≤ x :=
@@ -258,7 +261,7 @@ protected lemma zero_le : ∀ x : M, 0 ≤ x :=
   exact h
 
 lemma zero_lt_one : (0 : M) < 1 := by
-  simpa [models_iff] using Theory.models M _ PeanoMinus.zeroLtOne
+  exact models_iff.mp (Theory.models M _ PeanoMinus.zeroLtOne)
 
 lemma one_le_of_zero_lt : ∀ x : M, 0 < x → 1 ≤ x :=
   by
@@ -272,34 +275,45 @@ lemma one_le_of_zero_lt : ∀ x : M, 0 < x → 1 ≤ x :=
   exact h
 
 lemma add_lt_add : ∀ x y z : M, x < y → x + z < y + z := by
-  simpa [models_iff] using Theory.models M _ PeanoMinus.addLtAdd
+  have h := Theory.models M _ PeanoMinus.addLtAdd
+  simp only [models_iff, Semiformula.eval_all, LogicalConnective.HomClass.map_imply,
+    LogicalConnective.Prop.arrow_eq] at h
+  exact h
 
 protected lemma mul_zero' : ∀ x : M, x * 0 = 0 := by
-  simpa [models_iff] using Theory.models M _ PeanoMinus.mulZero
+  exact models_iff.mp (Theory.models M _ PeanoMinus.mulZero)
 
 protected lemma mul_one : ∀ x : M, x * 1 = x := by
-  simpa [models_iff] using Theory.models M _ PeanoMinus.mulOne
+  exact models_iff.mp (Theory.models M _ PeanoMinus.mulOne)
 
 protected lemma mul_assoc : ∀ x y z : M, (x * y) * z = x * (y * z) := by
-  simpa [models_iff] using Theory.models M _ PeanoMinus.mulAssoc
+  exact models_iff.mp (Theory.models M _ PeanoMinus.mulAssoc)
 
 protected lemma mul_comm : ∀ x y : M, x * y = y * x := by
-  simpa [models_iff] using Theory.models M _ PeanoMinus.mulComm
+  exact models_iff.mp (Theory.models M _ PeanoMinus.mulComm)
 
 lemma mul_lt_mul : ∀ x y z : M, x < y → 0 < z → x * z < y * z := by
-  simpa [models_iff] using Theory.models M _ PeanoMinus.mulLtMul
+  have h := Theory.models M _ PeanoMinus.mulLtMul
+  simp only [models_iff, Semiformula.eval_all, LogicalConnective.HomClass.map_imply,
+    LogicalConnective.Prop.arrow_eq,
+    LogicalConnective.HomClass.map_and, LogicalConnective.Prop.and_eq, and_imp] at h
+  exact h
 
 lemma mul_add_distr : ∀ x y z : M, x * (y + z) = x * y + x * z := by
-  simpa [models_iff] using Theory.models M _ PeanoMinus.distr
+  exact models_iff.mp (Theory.models M _ PeanoMinus.distr)
 
 lemma lt_irrefl : ∀ x : M, ¬x < x := by
-  simpa [models_iff] using Theory.models M _ PeanoMinus.ltIrrefl
+  exact models_iff.mp (Theory.models M _ PeanoMinus.ltIrrefl)
 
 protected lemma lt_trans : ∀ x y z : M, x < y → y < z → x < z := by
-  simpa [models_iff] using Theory.models M _ PeanoMinus.ltTrans
+  have h := Theory.models M _ PeanoMinus.ltTrans
+  simp only [models_iff, Semiformula.eval_all, LogicalConnective.HomClass.map_imply,
+    LogicalConnective.Prop.arrow_eq,
+    LogicalConnective.HomClass.map_and, LogicalConnective.Prop.and_eq, and_imp] at h
+  exact h
 
 lemma lt_tri : ∀ x y : M, x < y ∨ x = y ∨ y < x := by
-  simpa [models_iff] using Theory.models M _ PeanoMinus.ltTri
+  exact models_iff.mp (Theory.models M _ PeanoMinus.ltTri)
 
 /-- The inst Add Comm Monoid lean Pool construction in `FFL.FirstOrder.Arithmetic`. -/
 scoped instance instAddCommMonoidModel : AddCommMonoid M
diff --git a/LeanPool/PointwiseComposition/Foundation/FirstOrder/LJ/Basic.lean b/LeanPool/PointwiseComposition/Foundation/FirstOrder/LJ/Basic.lean
index 576de8d7a0..22a462176a 100644
--- a/LeanPool/PointwiseComposition/Foundation/FirstOrder/LJ/Basic.lean
+++ b/LeanPool/PointwiseComposition/Foundation/FirstOrder/LJ/Basic.lean
@@ -311,14 +311,67 @@ lemma height_cast {Γ Δ : Sequent L} {Ξ Λ : Head L} (d : Γ ⊢ᴸᴶ¹ Ξ) (
   subst Λ
   rfl
 
+section
+
+-- Realize the existing equation API before simplifying dependent derivations.
+attribute [local simp] height
+
 /-- Term substitution preserves derivation height (standard syntactic property). -/
 @[simp]
 lemma height_rewrite (f : ℕ → SyntacticTerm L) {Γ : Sequent L} {Ξ : Head L} (d : Γ ⊢ᴸᴶ¹ Ξ) :
     height (d.rewrite f) = height d :=
   by
-  induction d generalizing f <;> simp only [LJ.Derivation.rewrite, height, height_cast]
-  case positiveAnd a b iha ihb => exact congrArg (· + 1) <| congrArg₂ max (iha f) (ihb f)
-  all_goals aesop
+  induction d generalizing f <;> simp only [LJ.Derivation.rewrite, height_cast]
+  case identity => rfl
+  case verum => rfl
+  case falsum => rfl
+  case cut a b iha ihb =>
+    change max (height _) (height _) + 1 = max (height a) (height b) + 1
+    simpa only [height_cast] using congrArg (· + 1) (congrArg₂ max (iha _) (ihb _))
+  case contraction a ih =>
+    change height _ + 1 = height a + 1
+    simpa only [height_cast] using congrArg (· + 1) (ih _)
+  case weakening a ih =>
+    change height _ + 1 = height a + 1
+    simpa only [height_cast] using congrArg (· + 1) (ih _)
+  case weakeningRight a ih =>
+    change height _ + 1 = height a + 1
+    exact congrArg (· + 1) (ih f)
+  case positiveImply a ih =>
+    change height _ + 1 = height a + 1
+    simpa only [height_cast] using congrArg (· + 1) (ih _)
+  case negativeImply a b iha ihb =>
+    change max (height _) (height _) + 1 = max (height a) (height b) + 1
+    simpa only [height_cast] using congrArg (· + 1) (congrArg₂ max (iha _) (ihb _))
+  case positiveAnd a b iha ihb =>
+    change max (height _) (height _) + 1 = max (height a) (height b) + 1
+    exact congrArg (· + 1) (congrArg₂ max (iha f) (ihb f))
+  case negativeAnd a ih =>
+    change height _ + 1 = height a + 1
+    simpa only [height_cast] using congrArg (· + 1) (ih _)
+  case positiveOrLeft a ih =>
+    change height _ + 1 = height a + 1
+    exact congrArg (· + 1) (ih f)
+  case positiveOrRight a ih =>
+    change height _ + 1 = height a + 1
+    exact congrArg (· + 1) (ih f)
+  case negativeOr a b iha ihb =>
+    change max (height _) (height _) + 1 = max (height a) (height b) + 1
+    simpa only [height_cast] using congrArg (· + 1) (congrArg₂ max (iha _) (ihb _))
+  case positiveForall a ih =>
+    change height _ + 1 = height a + 1
+    simpa only [height_cast] using congrArg (· + 1) (ih _)
+  case negativeForall a ih =>
+    change height _ + 1 = height a + 1
+    simpa only [height_cast] using congrArg (· + 1) (ih _)
+  case positiveExists a ih =>
+    change height _ + 1 = height a + 1
+    simpa only [height_cast] using congrArg (· + 1) (ih _)
+  case negativeExists a ih =>
+    change height _ + 1 = height a + 1
+    simpa only [height_cast] using congrArg (· + 1) (ih _)
+
+end
 
 /-- The map construction in `FFL.FirstOrder.LJ.Derivation`. -/
 protected def map (d : Γ ⊢ᴸᴶ¹ Ξ) (f : ℕ → ℕ) :