diff --git a/Cslib.lean b/Cslib.lean
index 4d3aa37f9..fc9515419 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -49,6 +49,7 @@ public import Cslib.Foundations.Data.OmegaSequence.Flatten
 public import Cslib.Foundations.Data.OmegaSequence.InfOcc
 public import Cslib.Foundations.Data.OmegaSequence.Init
 public import Cslib.Foundations.Data.OmegaSequence.Temporal
+public import Cslib.Foundations.Data.Part
 public import Cslib.Foundations.Data.RelatesInSteps
 public import Cslib.Foundations.Data.Relation
 public import Cslib.Foundations.Data.Set.Saturation
@@ -78,6 +79,7 @@ public import Cslib.Languages.CombinatoryLogic.Confluence
 public import Cslib.Languages.CombinatoryLogic.Defs
 public import Cslib.Languages.CombinatoryLogic.Evaluation
 public import Cslib.Languages.CombinatoryLogic.List
+public import Cslib.Languages.CombinatoryLogic.PartrecToSKI
 public import Cslib.Languages.CombinatoryLogic.Recursion
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Context
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Basic
diff --git a/Cslib/Foundations/Data/Part.lean b/Cslib/Foundations/Data/Part.lean
new file mode 100644
index 000000000..97da80f6d
--- /dev/null
+++ b/Cslib/Foundations/Data/Part.lean
@@ -0,0 +1,31 @@
+/-
+Copyright (c) 2026 Jesse Alama. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jesse Alama
+-/
+
+module
+
+public import Cslib.Init
+public import Mathlib.Data.Part
+
+@[expose] public section
+
+/-!
+# Auxiliary lemmas for `Part`
+
+Convenience lemmas for working with partial values from `Mathlib.Data.Part`.
+
+Note: this file may go away entirely if leanprover-community/mathlib4#37521 gets merged.
+-/
+
+namespace Part
+
+/-- Extract witnesses from a bind that equals `Part.some`. -/
+theorem eq_some_of_bind_eq_some {a : Part α} {g : α → Part β} {m : β}
+    (h : (a >>= g) = Part.some m) :
+    ∃ x, a = Part.some x ∧ g x = Part.some m := by
+  have hm := Part.mem_bind_iff.mp (h ▸ Part.mem_some m)
+  exact hm.imp fun x ⟨hx, hm⟩ => ⟨Part.eq_some_iff.mpr hx, Part.eq_some_iff.mpr hm⟩
+
+end Part
diff --git a/Cslib/Languages/CombinatoryLogic/PartrecToSKI.lean b/Cslib/Languages/CombinatoryLogic/PartrecToSKI.lean
new file mode 100644
index 000000000..3e4b89894
--- /dev/null
+++ b/Cslib/Languages/CombinatoryLogic/PartrecToSKI.lean
@@ -0,0 +1,308 @@
+/-
+Copyright (c) 2026 Jesse Alama. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jesse Alama
+-/
+
+module
+
+public import Cslib.Foundations.Data.Part
+public import Cslib.Languages.CombinatoryLogic.Recursion
+public import Mathlib.Computability.PartrecCode
+
+@[expose] public section
+
+/-!
+# Partial Recursive → SKI-computable (Nat.Partrec)
+
+This file defines a notion of computability for SKI terms on natural numbers
+(using Church numerals) and translates `Nat.Partrec.Code` to SKI terms.
+
+## Main definitions
+
+- `Computes t f`: SKI term `t` computes a partial function `f : ℕ →. ℕ` on Church numerals.
+- `codeToSKINat`: translates `Nat.Partrec.Code` constructors to SKI terms.
+
+## Main results
+
+- `codeToSKINat_correct`: each translated code computes the corresponding `Code.eval`.
+- `natPartrec_skiComputable`: every `Nat.Partrec` function is SKI-computable.
+
+-/
+
+namespace Cslib
+
+namespace SKI
+
+open Red MRed
+open Nat.Partrec
+
+/-! ### Computability predicate for functions on ℕ -/
+
+/-- An SKI term `t` computes a partial function `f : ℕ →. ℕ` if,
+for every Church numeral input, `t` applied to the input is a Church numeral
+for the output whenever `f` is defined. -/
+def Computes (t : SKI) (f : ℕ →. ℕ) : Prop :=
+  ∀ n : ℕ, ∀ cn : SKI, IsChurch n cn →
+    ∀ m : ℕ, f n = Part.some m →
+      IsChurch m (t ⬝ cn)
+
+/-! ### Helper terms for `Code.prec` and `Code.rfind'` -/
+
+/-- Step function for primitive recursion:
+    `λ a cn prev. tg ⬝ (NatPair ⬝ a ⬝ (NatPair ⬝ (Pred ⬝ cn) ⬝ prev))`
+    Variables: &0 = a, &1 = cn, &2 = prev -/
+def PrecStepPoly (tg : SKI) : SKI.Polynomial 3 :=
+  tg ⬝' (NatPair ⬝' &0 ⬝' (NatPair ⬝' (Pred ⬝' &1) ⬝' &2))
+
+/-- SKI term for the primitive recursion step function. -/
+def PrecStep (tg : SKI) : SKI := (PrecStepPoly tg).toSKI
+
+theorem precStep_def (tg a cn prev : SKI) :
+    (PrecStep tg ⬝ a ⬝ cn ⬝ prev) ↠
+      tg ⬝ (NatPair ⬝ a ⬝ (NatPair ⬝ (Pred ⬝ cn) ⬝ prev)) :=
+  (PrecStepPoly tg).toSKI_correct [a, cn, prev] (by simp)
+
+/-- Full primitive recursion translation:
+    `λ n. Rec (tf (left n)) (PrecStep tg (left n)) (right n)` -/
+def PrecTransPoly (tf tg : SKI) : SKI.Polynomial 1 :=
+  Rec ⬝' (tf ⬝' (NatUnpairLeft ⬝' &0))
+      ⬝' (PrecStep tg ⬝' (NatUnpairLeft ⬝' &0))
+      ⬝' (NatUnpairRight ⬝' &0)
+
+/-- SKI term for primitive recursion via `Rec` with pair/unpair plumbing. -/
+def PrecTrans (tf tg : SKI) : SKI := (PrecTransPoly tf tg).toSKI
+
+theorem precTrans_def (tf tg cn : SKI) :
+    (PrecTrans tf tg ⬝ cn) ↠
+      Rec ⬝ (tf ⬝ (NatUnpairLeft ⬝ cn))
+          ⬝ (PrecStep tg ⬝ (NatUnpairLeft ⬝ cn))
+          ⬝ (NatUnpairRight ⬝ cn) :=
+  (PrecTransPoly tf tg).toSKI_correct [cn] (by simp)
+
+/-- Unbounded search translation:
+    `λ n. RFindAbove ⬝ (NatUnpairRight ⬝ n) ⬝ (B ⬝ tf ⬝ (NatPair ⬝ (NatUnpairLeft ⬝ n)))` -/
+def RFindTransPoly (tf : SKI) : SKI.Polynomial 1 :=
+  RFindAbove ⬝' (NatUnpairRight ⬝' &0)
+             ⬝' (B ⬝' tf ⬝' (NatPair ⬝' (NatUnpairLeft ⬝' &0)))
+
+/-- SKI term for unbounded search (μ-recursion). -/
+def RFindTrans (tf : SKI) : SKI := (RFindTransPoly tf).toSKI
+
+theorem rfindTrans_def (tf cn : SKI) :
+    (RFindTrans tf ⬝ cn) ↠
+      RFindAbove ⬝ (NatUnpairRight ⬝ cn)
+                 ⬝ (B ⬝ tf ⬝ (NatPair ⬝ (NatUnpairLeft ⬝ cn))) :=
+  (RFindTransPoly tf).toSKI_correct [cn] (by simp)
+
+/-! ### Translation from Nat.Partrec.Code to SKI -/
+
+/-- Translate `Nat.Partrec.Code` to SKI terms operating on Church numerals. -/
+def codeToSKINat : Code → SKI
+  | .zero => K ⬝ SKI.Zero
+  | .succ => SKI.Succ
+  | .left => NatUnpairLeft
+  | .right => NatUnpairRight
+  | .pair f g =>
+    let tf := codeToSKINat f
+    let tg := codeToSKINat g
+    S ⬝ (B ⬝ NatPair ⬝ tf) ⬝ tg
+  | .comp f g =>
+    B ⬝ (codeToSKINat f) ⬝ (codeToSKINat g)
+  | .prec f g =>
+    PrecTrans (codeToSKINat f) (codeToSKINat g)
+  | .rfind' f =>
+    RFindTrans (codeToSKINat f)
+
+/-! ### Correctness proofs -/
+
+/-- Helper for total functions: if `c.eval` is total with output `g n`, and `t` reduces
+    to a Church numeral for `g n`, then `t` computes `c.eval`. -/
+private theorem computes_of_total (t : SKI) (c : Code) (g : ℕ → ℕ)
+    (heval : ∀ n, c.eval n = Part.some (g n))
+    (hcorrect : ∀ n cn, IsChurch n cn → IsChurch (g n) (t ⬝ cn)) :
+    Computes t c.eval := by
+  intro n cn hcn m hm; rw [heval] at hm; obtain rfl := Part.some_injective hm
+  exact hcorrect n cn hcn
+
+/-- `Code.zero` computes the constant zero function. -/
+theorem zero_computes : Computes (K ⬝ SKI.Zero) (Code.eval .zero) :=
+  computes_of_total _ .zero (fun _ => 0)
+    (fun n => by rw [show Code.zero = Code.const 0 from rfl, Code.eval_const])
+    (fun _ _ _ => isChurch_trans 0 (MRed.K SKI.Zero _) zero_correct)
+
+/-- `Code.succ` computes the successor function. -/
+theorem succ_computes : Computes SKI.Succ (Code.eval .succ) :=
+  computes_of_total _ .succ (· + 1)
+    (fun _ => by simp only [Code.eval, PFun.coe_val])
+    (fun n cn hcn => succ_correct n cn hcn)
+
+/-- `Code.left` computes the left projection of `Nat.unpair`. -/
+theorem left_computes : Computes NatUnpairLeft (Code.eval .left) :=
+  computes_of_total _ .left (fun n => (Nat.unpair n).1)
+    (fun _ => by simp only [Code.eval, PFun.coe_val])
+    (fun n cn hcn => natUnpairLeft_correct n cn hcn)
+
+/-- `Code.right` computes the right projection of `Nat.unpair`. -/
+theorem right_computes : Computes NatUnpairRight (Code.eval .right) :=
+  computes_of_total _ .right (fun n => (Nat.unpair n).2)
+    (fun _ => by simp only [Code.eval, PFun.coe_val])
+    (fun n cn hcn => natUnpairRight_correct n cn hcn)
+
+/-- Composition of computable functions is computable. -/
+theorem comp_computes {f g : ℕ →. ℕ} {tf tg : SKI}
+    (hf : Computes tf f) (hg : Computes tg g) :
+    Computes (B ⬝ tf ⬝ tg) (fun n => g n >>= f) := by
+  intro n cn hcn m hm
+  obtain ⟨intermediate, hint_eq, hm_eq⟩ := Part.eq_some_of_bind_eq_some hm
+  exact isChurch_trans _ (B_def tf tg cn)
+    (hf intermediate (tg ⬝ cn) (hg n cn hcn intermediate hint_eq) m hm_eq)
+
+/-- Pairing of computable functions is computable. -/
+theorem pair_computes {f g : ℕ →. ℕ} {tf tg : SKI}
+    (hf : Computes tf f) (hg : Computes tg g) :
+    Computes (S ⬝ (B ⬝ NatPair ⬝ tf) ⬝ tg)
+      (fun n => Nat.pair <$> f n <*> g n) := by
+  intro n cn hcn m hm
+  simp only at hm
+  obtain ⟨h, hh_mem, hm_in_h⟩ := Part.mem_bind_iff.mp (hm ▸ Part.mem_some m)
+  obtain ⟨a, ha_mem, rfl⟩ := (Part.mem_map_iff _).mp hh_mem
+  obtain ⟨b, hb_mem, rfl⟩ := (Part.mem_map_iff _).mp hm_in_h
+  have hca := hf n cn hcn a (Part.eq_some_iff.mpr ha_mem)
+  have hcb := hg n cn hcn b (Part.eq_some_iff.mpr hb_mem)
+  exact isChurch_trans _ ((MRed.S _ _ _).trans (MRed.head _ (B_def _ _ _)))
+    (natPair_correct a b _ _ hca hcb)
+
+/-- Helper: `Rec` correctly implements primitive recursion from `Code.prec`. -/
+private theorem prec_rec_correct (f g : Code) (tf tg : SKI)
+    (ihf : Computes tf f.eval) (ihg : Computes tg g.eval)
+    (a₀ : ℕ) (ca : SKI) (hca : IsChurch a₀ ca) :
+    ∀ b₀ : ℕ, ∀ m : ℕ,
+    Code.eval (f.prec g) (Nat.pair a₀ b₀) = Part.some m →
+    ∀ cb : SKI, IsChurch b₀ cb →
+    IsChurch m (Rec ⬝ (tf ⬝ ca) ⬝ (PrecStep tg ⬝ ca) ⬝ cb) := by
+  intro b₀
+  induction b₀ with
+  | zero =>
+    intro m hm cb hcb
+    rw [Code.eval_prec_zero] at hm
+    exact isChurch_trans _ (rec_zero _ _ cb hcb) (ihf a₀ ca hca m hm)
+  | succ k ih =>
+    intro m hm cb hcb
+    rw [Code.eval_prec_succ] at hm
+    obtain ⟨ih_val, hih_eq, hm_eq⟩ := Part.eq_some_of_bind_eq_some hm
+    -- By IH, Rec computes the intermediate value on Pred ⬝ cb
+    have hpred : IsChurch k (Pred ⬝ cb) := pred_correct (k + 1) cb hcb
+    set step := PrecStep tg ⬝ ca
+    set base := tf ⬝ ca
+    have hcih := ih ih_val hih_eq (Pred ⬝ cb) hpred
+    -- Build Church numeral for the argument to g
+    have hpair_inner := natPair_correct k ih_val (Pred ⬝ cb)
+      (Rec ⬝ base ⬝ step ⬝ (Pred ⬝ cb)) hpred hcih
+    have hpair_full := natPair_correct a₀ (Nat.pair k ih_val) ca
+      (NatPair ⬝ (Pred ⬝ cb) ⬝ (Rec ⬝ base ⬝ step ⬝ (Pred ⬝ cb))) hca hpair_inner
+    -- By ihg, tg computes the result
+    have hcm := ihg _ _ hpair_full m hm_eq
+    -- Chain the reductions
+    have hred := (rec_succ k base step cb hcb).trans
+      (precStep_def tg ca cb (Rec ⬝ base ⬝ step ⬝ (Pred ⬝ cb)))
+    exact isChurch_trans _ hred hcm
+
+/-- If `k ∈ Nat.rfind …`, then `f` evaluates to 0 at the root. -/
+private theorem rfind_eval_root {f : Code} {a₀ m₀ k : ℕ}
+    (hk : k ∈ Nat.rfind (fun n =>
+      (fun m => decide (m = 0)) <$> f.eval (Nat.pair a₀ (n + m₀)))) :
+    f.eval (Nat.pair a₀ (m₀ + k)) = Part.some 0 := by
+  have hspec := Nat.rfind_spec hk
+  obtain ⟨val, hval_mem, hval_eq⟩ := (Part.mem_map_iff _).mp hspec
+  have : val = 0 := by simpa using hval_eq
+  subst this; rw [Nat.add_comm] at hval_mem
+  exact Part.eq_some_iff.mpr hval_mem
+
+/-- If `k ∈ Nat.rfind …`, then `f` evaluates to a nonzero value below `k`. -/
+private theorem rfind_eval_pos_below {f : Code} {a₀ m₀ k : ℕ}
+    (hk : k ∈ Nat.rfind (fun n =>
+      (fun m => decide (m = 0)) <$> f.eval (Nat.pair a₀ (n + m₀)))) :
+    ∀ i < k, ∃ vi, vi ≠ 0 ∧ f.eval (Nat.pair a₀ (m₀ + i)) = Part.some vi := by
+  intro i hi
+  have hmin := Nat.rfind_min hk hi
+  obtain ⟨val, hval_mem, hval_eq⟩ := (Part.mem_map_iff _).mp hmin
+  have hval_ne : val ≠ 0 := by simpa using hval_eq
+  rw [Nat.add_comm] at hval_mem
+  exact ⟨val, hval_ne, Part.eq_some_iff.mpr hval_mem⟩
+
+/-- Primitive recursion of computable functions is computable. -/
+private theorem prec_computes {f g : Code} {tf tg : SKI}
+    (ihf : Computes tf f.eval) (ihg : Computes tg g.eval) :
+    Computes (PrecTrans tf tg) (f.prec g).eval := by
+  intro n cn hcn m hm
+  have hca := natUnpairLeft_correct n cn hcn
+  have hcb := natUnpairRight_correct n cn hcn
+  have hred := precTrans_def tf tg cn
+  have hpair : n = Nat.pair (Nat.unpair n).1 (Nat.unpair n).2 :=
+    (Nat.pair_unpair n).symm
+  rw [hpair] at hm
+  exact isChurch_trans _ hred (prec_rec_correct f g _ _ ihf ihg
+    (Nat.unpair n).1 (NatUnpairLeft ⬝ cn) hca
+    (Nat.unpair n).2 m hm (NatUnpairRight ⬝ cn) hcb)
+
+/-- Unbounded search of a computable function is computable. -/
+private theorem rfind_computes {f : Code} {tf : SKI}
+    (ihf : Computes tf f.eval) :
+    Computes (RFindTrans tf) (Code.rfind' f).eval := by
+  intro n cn hcn result hresult
+  set a₀ := (Nat.unpair n).1
+  set m₀ := (Nat.unpair n).2
+  have hca := natUnpairLeft_correct n cn hcn
+  have hcm₀ := natUnpairRight_correct n cn hcn
+  -- Extract k from the rfind result
+  have hresult' : result ∈ Code.eval (Code.rfind' f) n := by
+    rw [hresult]; exact Part.mem_some _
+  simp only [Code.eval, Nat.unpaired,
+    show (Nat.unpair n).1 = a₀ from rfl,
+    show (Nat.unpair n).2 = m₀ from rfl] at hresult'
+  obtain ⟨k, hk_mem, hresult_eq⟩ := (Part.mem_map_iff _).mp hresult'
+  subst hresult_eq
+  -- Build the callback: the composed SKI term computes f on paired arguments
+  set g := B ⬝ tf ⬝ (NatPair ⬝ (NatUnpairLeft ⬝ cn))
+  have hg : ∀ i y, IsChurch i y → ∀ v, f.eval (Nat.pair a₀ i) = Part.some v →
+      IsChurch v (g ⬝ y) := fun i y hy v hv =>
+    isChurch_trans _ (B_def tf (NatPair ⬝ (NatUnpairLeft ⬝ cn)) y)
+      (ihf _ _ (natPair_correct a₀ i (NatUnpairLeft ⬝ cn) y hca hy) v hv)
+  -- Apply generalized RFindAbove_correct'
+  have hind := RFindAbove_correct' g (NatUnpairRight ⬝ cn) k m₀ hcm₀
+    (fun y hy => hg (m₀ + k) y hy 0 (rfind_eval_root hk_mem))
+    (fun i hi y hy => by
+      obtain ⟨vi, hvi_ne, hvi_eq⟩ := rfind_eval_pos_below hk_mem i hi
+      exact ⟨vi - 1, by have : vi - 1 + 1 = vi := by omega
+                        rw [this]; exact hg (m₀ + i) y hy vi hvi_eq⟩)
+  rw [Nat.add_comm] at hind
+  exact isChurch_trans _ (rfindTrans_def tf cn) hind
+
+/-- Main correctness theorem: `codeToSKINat` correctly computes `Code.eval`. -/
+theorem codeToSKINat_correct (c : Code) : Computes (codeToSKINat c) c.eval := by
+  induction c with
+  | zero => exact zero_computes
+  | succ => exact succ_computes
+  | left => exact left_computes
+  | right => exact right_computes
+  | pair f g ihf ihg =>
+    simp only [codeToSKINat, Code.eval]; exact pair_computes ihf ihg
+  | comp f g ihf ihg =>
+    simp only [codeToSKINat, Code.eval]; exact comp_computes ihf ihg
+  | prec f g ihf ihg =>
+    simp only [codeToSKINat]; exact prec_computes ihf ihg
+  | rfind' f ihf =>
+    simp only [codeToSKINat]; exact rfind_computes ihf
+
+/-! ### Main result -/
+
+/-- Every partial recursive function on `ℕ` is SKI-computable. -/
+theorem natPartrec_skiComputable (f : ℕ →. ℕ) (hf : Nat.Partrec f) :
+    ∃ t : SKI, Computes t f := by
+  obtain ⟨c, hc⟩ := Code.exists_code.mp hf
+  exact ⟨codeToSKINat c, hc ▸ codeToSKINat_correct c⟩
+
+end SKI
+
+end Cslib
diff --git a/Cslib/Languages/CombinatoryLogic/Recursion.lean b/Cslib/Languages/CombinatoryLogic/Recursion.lean
index 5885b0d74..d021ac3a0 100644
--- a/Cslib/Languages/CombinatoryLogic/Recursion.lean
+++ b/Cslib/Languages/CombinatoryLogic/Recursion.lean
@@ -253,7 +253,7 @@ We define Rec so that
 -/
 def Rec : SKI := fixedPoint RecAux
 theorem rec_def (x g a : SKI) :
-    (Rec ⬝ x ⬝ g ⬝ a) ↠ SKI.Cond ⬝ x ⬝ (g ⬝ a ⬝ (Rec ⬝ x ⬝ g ⬝ (Pred ⬝ a))) ⬝ (IsZero ⬝ a) := calc
+  (Rec ⬝ x ⬝ g ⬝ a) ↠ SKI.Cond ⬝ x ⬝ (g ⬝ a ⬝ (Rec ⬝ x ⬝ g ⬝ (Pred ⬝ a))) ⬝ (IsZero ⬝ a) := calc
   _ ↠ RecAux ⬝ Rec ⬝ x ⬝ g ⬝ a := by
       apply MRed.head; apply MRed.head; apply MRed.head
       apply fixedPoint_correct
@@ -305,27 +305,47 @@ theorem rfindAboveAux_step (R₀ f a : SKI) {m : Nat} (hfa : IsChurch (m + 1) (f
 
 /-- Find the minimal root of `fNat` above a number n -/
 def RFindAbove : SKI := RFindAboveAux.fixedPoint
+
+/-- One unfolding of `RFindAbove`: apply the fixed-point combinator once. -/
+theorem RFindAbove_unfold (x g : SKI) :
+    (RFindAbove ⬝ x ⬝ g) ↠ RFindAboveAux ⬝ RFindAbove ⬝ x ⬝ g := by
+  apply MRed.head; apply MRed.head; exact fixedPoint_correct _
+
+/-- Generalized root-finding that works with pointwise properties rather than a total
+    function. At the root `m + n`, `f` yields Church 0; below, a nonzero Church numeral. -/
+theorem RFindAbove_correct' (f x : SKI) (n m : Nat) (hx : IsChurch m x)
+    (hf_root : ∀ y, IsChurch (m + n) y → IsChurch 0 (f ⬝ y))
+    (hf_below : ∀ i < n, ∀ y, IsChurch (m + i) y →
+      ∃ k, IsChurch (k + 1) (f ⬝ y)) :
+    IsChurch (m + n) (RFindAbove ⬝ x ⬝ f) := by
+  induction n generalizing m x
+  all_goals apply isChurch_trans _ (RFindAbove_unfold x f)
+  case zero =>
+    simp only [Nat.add_zero] at *
+    apply isChurch_trans (a' := x)
+    · exact rfindAboveAux_base _ _ _ (hf_root x hx)
+    · exact hx
+  case succ n ih =>
+    apply isChurch_trans (a' := RFindAbove ⬝ (SKI.Succ ⬝ x) ⬝ f)
+    · obtain ⟨k, hk⟩ := hf_below 0 (by omega) x (by simpa using hx)
+      exact rfindAboveAux_step _ _ _ hk
+    · rw [show m + (n + 1) = (m + 1) + n from by omega]
+      exact ih (SKI.Succ ⬝ x) (m + 1) (succ_correct _ x hx)
+        (fun y hy => hf_root y (by rw [show m + 1 + n = m + (n + 1) from by omega] at hy; exact hy))
+        (fun i hi y hy => hf_below (i + 1) (by omega) y (by
+          rw [show m + 1 + i = m + (i + 1) from by omega] at hy; exact hy))
+
 theorem RFindAbove_correct (fNat : Nat → Nat) (f x : SKI)
-    (hf : ∀ i : Nat, ∀ y : SKI, IsChurch i y →  IsChurch (fNat i) (f ⬝ y))
+    (hf : ∀ i : Nat, ∀ y : SKI, IsChurch i y → IsChurch (fNat i) (f ⬝ y))
     (n m : Nat) (hx : IsChurch m x) (hroot : fNat (m+n) = 0) (hpos : ∀ i < n, fNat (m+i) ≠ 0) :
     IsChurch (m+n) (RFindAbove ⬝ x ⬝ f) := by
-  induction n generalizing m x
-  all_goals apply isChurch_trans (a' := RFindAboveAux ⬝ RFindAbove ⬝ x ⬝ f)
-  case zero.a =>
-    apply isChurch_trans (a' := x) <;>
-      grind [rfindAboveAux_base]
-  case succ.a n ih =>
-    apply isChurch_trans (a' := RFindAbove ⬝ (SKI.Succ ⬝ x) ⬝ f)
-    · let y := (fNat m).pred
-      have : IsChurch (y + 1) (f ⬝ x) := by
-        subst y
-        exact Nat.succ_pred_eq_of_ne_zero (hpos 0 (by simp)) ▸ hf m x hx
-      apply rfindAboveAux_step
-      assumption
-    · replace ih := ih (SKI.Succ ⬝ x) (m + 1) (succ_correct _ x hx)
-      grind
-  -- close the `h` goals of the above `apply isChurch_trans`
-  all_goals {apply MRed.head; apply MRed.head; exact fixedPoint_correct _}
+  apply RFindAbove_correct' f x n m hx
+  · intro y hy; exact hroot ▸ hf (m + n) y hy
+  · intro i hi y hy
+    have hne := hpos i hi
+    refine ⟨(fNat (m + i)) - 1, ?_⟩
+    have : fNat (m + i) - 1 + 1 = fNat (m + i) := by omega
+    rw [this]; exact hf (m + i) y hy
 
 
 /-- Ordinary root finding is root finding above zero -/