diff --git a/src/Telomare.hs b/src/Telomare.hs
index cc3ffeb..0241ee0 100644
--- a/src/Telomare.hs
+++ b/src/Telomare.hs
@@ -131,6 +131,7 @@ data ParserTerm l v
   | TRight (ParserTerm l v)
   | TTrace (ParserTerm l v)
   | THash (ParserTerm l v)
+  | TChurch Int
   | TLam (LamType l) (ParserTerm l v)
   | TLimitedRecursion (ParserTerm l v) (ParserTerm l v) (ParserTerm l v)
   deriving (Eq, Ord, Functor, Foldable, Traversable)
@@ -174,6 +175,7 @@ instance (Show l, Show v) => Show (ParserTerm l v) where
     alg (TRightF r) = indentWithOneChild "TRight" r
     alg (TTraceF x) = indentWithOneChild "TTrace" x
     alg (THashF x) = indentWithOneChild "THash" x
+    alg (TChurchF n) = sindent $ "TChurch " <> show n
     alg (TLamF l x) = indentWithOneChild ("TLam " <> show l) x
     alg (TLimitedRecursionF t r b) = indentWithThreeChildren "TLimitedRecursion" t  r  b
 
@@ -527,10 +529,34 @@ gateF x y = do
 iteF :: BreakState' a b -> BreakState' a b -> BreakState' a b -> BreakState' a b
 iteF x y z = setEnvF (pairF (gateF z y) x)
 
--- to construct a church numeral (\f x -> f ... (f x))
--- the new, optimized church numeral operation iterates on a function "frame" (rf, (rf, (f', (x, env'))))
+-- inside two lambdas, (\f x -> ...)
+-- creates and iterates on a function "frame" (rf, (rf, (f', (x, env'))))
 -- rf is the function to pull arguments out of the frame, run f', and construct the next frame
 -- (f',env') is f (since f may contain a saved environment/closure env we want to use for each iteration)
+repeatFunctionF :: (Show a, Enum b) => LocTag -> FragExpr a -> BreakState' a b
+repeatFunctionF l repeater =
+  let applyF = SetEnvFrag $ RightFrag EnvFrag
+      env' = RightFrag (RightFrag (RightFrag EnvFrag))
+      -- takes (rf, (f', (x, env'))), executes f' with (x, env') and creates a new frame
+      rf = deferF . pure . tag l $
+                 PairFrag (LeftFrag EnvFrag)
+                          (PairFrag (LeftFrag EnvFrag)
+                                    (PairFrag (LeftFrag (RightFrag EnvFrag))
+                                              (PairFrag applyF env')))
+      x = pure . tag l $ LeftFrag EnvFrag
+      f' = pure . tag l . LeftFrag . LeftFrag $ RightFrag EnvFrag
+      fenv = pure . tag l . RightFrag . LeftFrag $ RightFrag EnvFrag
+      -- (x, ((f', fenv), 0)) -> (rf, (rf, (f', (x, fenv))))
+      frameSetup = rf >>= (\rf' -> pairF (pure rf') (pairF (pure rf') (pairF f' (pairF x fenv))))
+      -- run the iterations x' number of times, then unwrap the result from the final frame
+      unwrapFrame = LeftFrag . RightFrag . RightFrag . RightFrag $ repeater
+  in clamF (lamF (setEnvF (pairF (deferF (pure . tag l $ unwrapFrame)) frameSetup)))
+
+-- to construct a church numeral (\f x -> f ... (f x))
+-- the core is nested setenvs around an env, where the number of setenvs is magnitude of church numeral
+i2cF :: (Show a, Enum b) => LocTag -> Int -> BreakState' a b
+i2cF l n = repeatFunctionF l (iterate SetEnvFrag EnvFrag !! n)
+
 unsizedRecursionWrapper :: UnsizedRecursionToken
                         -> BreakState' RecursionPieceFrag UnsizedRecursionToken
                         -> BreakState' RecursionPieceFrag UnsizedRecursionToken
@@ -544,25 +570,9 @@ unsizedRecursionWrapper urToken t r b =
       fifthArgF = pure . tag DummyLoc . LeftFrag . RightFrag . RightFrag . RightFrag . RightFrag $ EnvFrag
       abortToken = pure . tag DummyLoc $ PairFrag ZeroFrag ZeroFrag
       abortFragF = pure $ DummyLoc :< AbortFragF
-      -- b is on the stack when this is called, so args are (i, (b, 0))
+      -- b is on the stack when this is called, so args are (i, (b, ...))
       abrt = lamF (setEnvF $ pairF (setEnvF (pairF abortFragF abortToken))
                                    (appF secondArgF firstArgF))
-      applyF = SetEnvFrag $ RightFrag EnvFrag
-      env' = RightFrag (RightFrag (RightFrag EnvFrag))
-      -- takes (rf, (f', (x, env'))), executes f' with (x, env') and creates a new frame
-      rf = deferF . pure . tag DummyLoc $
-        PairFrag (LeftFrag EnvFrag)
-                 (PairFrag (LeftFrag EnvFrag)
-                           (PairFrag (LeftFrag (RightFrag EnvFrag))
-                                     (PairFrag applyF env')))
-      -- construct the initial frame from f and x ((b, (rWrap, 0)) -> (rf, (rf, (f', (x, env')))))
-      frameSetup = do
-        rf' <- rf
-        pairF (pure rf') (pairF (pure rf') (pairF (pure . tag DummyLoc $ LeftFrag (LeftFrag (RightFrag EnvFrag)))
-                                  (pairF abrt (pure . tag DummyLoc $
-                                                RightFrag (LeftFrag (RightFrag EnvFrag))))))
-      -- run the iterations x' number of times, then unwrap the result from the final frame
-      unwrapFrame = LeftFrag . RightFrag . RightFrag . RightFrag . AuxFrag $ NestedSetEnvs urToken
       wrapU =  fmap ((DummyLoc :<) . AuxFragF . SizingWrapper urToken . FragExprUR)
       -- \t r b r' i -> if t i then r r' i else b i -- t r b are already on the stack when this is evaluated
       rWrap = lamF . lamF $ iteF (appF fifthArgF firstArgF)
@@ -570,9 +580,10 @@ unsizedRecursionWrapper urToken t r b =
                                  (appF thirdArgF firstArgF)
       -- hack to make sure recursion test wrapper can be put in a definite place when sizing
       tWrap = pairF (deferF $ appF secondArgF firstArgF) (pairF t . pure $ DummyLoc :< ZeroFragF)
-      churchNum = clamF (lamF (setEnvF (pairF (deferF (pure . tag DummyLoc $ unwrapFrame)) frameSetup)))
+      repeater = AuxFrag $ NestedSetEnvs urToken
+      churchNum = repeatFunctionF DummyLoc repeater
       trb = pairF b (pairF r (pairF tWrap (pure . tag DummyLoc $ ZeroFrag)))
-  in setEnvF . wrapU $ pairF (deferF $ appF (appF churchNum rWrap) firstArgF) trb
+  in setEnvF . wrapU $ pairF (deferF $ appF (appF churchNum rWrap) abrt) trb
 
 nextBreakToken :: (Enum b, Show b) => BreakState a b b
 nextBreakToken = do
diff --git a/src/Telomare/Resolver.hs b/src/Telomare/Resolver.hs
index 6e35ab0..68d826b 100644
--- a/src/Telomare/Resolver.hs
+++ b/src/Telomare/Resolver.hs
@@ -25,14 +25,14 @@ import Data.Map.Strict (Map, fromList, keys)
 import Data.Set (Set, (\\))
 import qualified Data.Set as Set
 import Debug.Trace (trace, traceShow, traceShowId)
-import PrettyPrint (TypeDebugInfo (..), showTypeDebugInfo)
+import PrettyPrint (TypeDebugInfo (..), showTypeDebugInfo, prettyPrint)
 import Telomare (BreakState', DataType (..), FragExpr (..), FragExprF (..),
                  FragExprUR (..), FragIndex (..), IExpr (..), IExprF (..),
                  LamType (..), LocTag (..), ParserTerm (..), ParserTermF (..),
                  PartialType (..), RecursionPieceFrag,
                  RecursionSimulationPieces (..), Term1 (..), Term2 (..),
                  Term3 (..), UnsizedRecursionToken, appF, clamF, deferF, forget,
-                 forgetAnnotationFragExprUR, gateF, lamF, nextBreakToken, pairF,
+                 forgetAnnotationFragExprUR, gateF, i2cF, lamF, nextBreakToken, pairF,
                  setEnvF, showRunBreakState', tag, unsizedRecursionWrapper,
                  varNF)
 import Telomare.Parser (AnnotatedUPT, Pattern (..), PatternF (..),
@@ -41,6 +41,12 @@ import Telomare.Parser (AnnotatedUPT, Pattern (..), PatternF (..),
                         parseWithPrelude)
 import Text.Megaparsec (errorBundlePretty, runParser)
 
+debug :: Bool
+debug = True
+
+debugTrace :: String -> a -> a
+debugTrace s x = if debug then trace s x else x
+
 type VarList = [String]
 
 -- |Int to ParserTerm
@@ -59,6 +65,7 @@ s2t :: LocTag -> String -> Cofree (ParserTermF l v) LocTag
 s2t anno = ints2t anno . fmap ord
 
 -- |Int to Church encoding
+{-
 i2c :: LocTag -> Int -> Term1
 i2c anno x = anno :< TLamF (Closed "f") (anno :< TLamF (Open "x") (inner x))
   where inner :: Int -> Term1
@@ -66,6 +73,7 @@ i2c anno x = anno :< TLamF (Closed "f") (anno :< TLamF (Open "x") (inner x))
         coalg :: Int -> Base Term1 (Either Term1 Int)
         coalg 0 = anno C.:< TVarF "x"
         coalg n = anno C.:< TAppF (Left . (anno :<) . TVarF $ "f") (Right $ n - 1)
+-}
 
 instance MonadFail (Either String) where
   fail = Left
@@ -271,6 +279,7 @@ debruijinize vl = \case
   (anno :< THashF x) -> (\y -> anno :< THashF y) <$> debruijinize vl x
   (anno :< TLamF (Open n) x) -> (\y -> anno :< TLamF (Open ()) y) <$> debruijinize (n : vl) x
   (anno :< TLamF (Closed n) x) -> (\y -> anno :< TLamF (Closed ()) y) <$> debruijinize (n : vl) x
+  (anno :< TChurchF n) -> pure $ anno :< TChurchF n
   (anno :< TLimitedRecursionF t r b) -> (\x y z -> anno :< TLimitedRecursionF x y z) <$> debruijinize vl t <*> debruijinize vl r <*> debruijinize vl b
 
 rewriteOuterTag :: anno -> Cofree a anno -> Cofree a anno
@@ -294,6 +303,7 @@ splitExpr' = \case
   (anno :< TTraceF x) -> rewriteOuterTag anno <$> setEnvF (pairF (deferF (pure . tag anno $ TraceFrag)) (splitExpr' x))
   (anno :< TLamF (Open ()) x) -> rewriteOuterTag anno <$> lamF (splitExpr' x)
   (anno :< TLamF (Closed ()) x) -> rewriteOuterTag anno <$> clamF (splitExpr' x)
+  (anno :< TChurchF n) -> i2cF anno n
   (anno :< TLimitedRecursionF t r b) ->
     rewriteOuterTag anno <$> (nextBreakToken >>=
       (\x -> unsizedRecursionWrapper x (splitExpr' t) (splitExpr' r) (splitExpr' b)))
@@ -364,7 +374,8 @@ validateVariables prelude term =
           (\x y z -> anno :< TLimitedRecursionF x y z) <$> validateWithEnvironment t
                                                        <*> validateWithEnvironment r
                                                        <*> validateWithEnvironment b
-        anno :< ChurchUPF n -> pure $ i2c anno n
+        -- anno :< ChurchUPF n -> pure $ i2c anno n
+        anno :< ChurchUPF n -> pure $ anno :< TChurchF n
         anno :< LeftUPF x -> (\y -> anno :< TLeftF y) <$> validateWithEnvironment x
         anno :< RightUPF x -> (\y -> anno :< TRightF y) <$> validateWithEnvironment x
         anno :< TraceUPF x -> (\y -> anno :< TTraceF y) <$> validateWithEnvironment x
@@ -433,7 +444,7 @@ addBuiltins aupt = DummyLoc :< LetUPF
 process :: [(String, AnnotatedUPT)] -- ^Prelude
         -> AnnotatedUPT
         -> Either String Term3
-process prelude upt = splitExpr <$> process2Term2 prelude upt
+process prelude upt = (\dt -> debugTrace ("Resolver process term:\n" <> prettyPrint dt) dt) . splitExpr <$> process2Term2 prelude upt
 
 process2Term2 :: [(String, AnnotatedUPT)] -- ^Prelude
               -> AnnotatedUPT