diff --git a/Yatima/Typechecker/Datatypes.lean b/Yatima/Typechecker/Datatypes.lean
index 4c0eb2ab..d4963e04 100644
--- a/Yatima/Typechecker/Datatypes.lean
+++ b/Yatima/Typechecker/Datatypes.lean
@@ -90,11 +90,20 @@ def TypedConst.type : TypedConst → TypedExpr
   | recursor    type ..
   | quotient    type .. => type
 
-structure Env' (SusValue : Type) where
-  exprs : List SusValue
+structure Env' (Value : Type) where
+  exprs : List Value
   univs : List Univ
   deriving Inhabited
 
+inductive ValueException where
+  | custom : String → ValueException
+  | noVar : ValueException
+deriving Inhabited
+
+instance : ToString ValueException where toString
+  | .custom e => s!"{e}"
+  | .noVar => s!"Free variable found. This means the encoding of the expression is incorrect"
+
 mutual
   /--
   Values are the final result of the evaluation of well-typed expressions under a well-typed
@@ -109,16 +118,17 @@ mutual
     We also keep the `TypeInfo` of each subapplication (`neu a_1 a_2 ... a_i`), for
     i = 0, .. , n-1; this preserves information necessary to implement the quoting
     (i.e. read-back) functionality that is used in lambda inference -/
-    | app : Neutral → List (AddInfo (Thunk Value)) → List TypeInfo → Value
+    | app : Neutral → List (AddInfo Value) → List TypeInfo → Value
     /-- Lambdas are unevaluated expressions with environments for their free
     variables apart from their argument variables -/
-    | lam : AddInfo (Thunk Value) → TypedExpr → Env' (AddInfo (Thunk Value)) → Value
-    /-- Pi types will have thunks for their domains and unevaluated expressions
+    | lam : AddInfo Value → TypedExpr → Env' (AddInfo Value) → Value
+    /-- Pi types will have values for their domains and unevaluated expressions
     analogous to lambda bodies for their codomains -/
-    | pi : AddInfo (Thunk Value) → TypedExpr → Env' (AddInfo (Thunk Value)) → Value
+    | pi  : AddInfo Value → TypedExpr → Env' (AddInfo Value) → Value
     | lit : Literal → Value
-    -- An exception constructor is used to catch bugs in the evaluator/typechecker
-    | exception : String → Value
+    -- An exception constructor is added so that we don't have to wrap `Exception` around `Value`.
+    -- This is both for convenience and efficiency.
+    | exception : ValueException → Value
     deriving Inhabited
   /--
   A neutral term is either a variable or a constant with not enough arguments to
@@ -134,14 +144,6 @@ end
 
 abbrev TypedValue := AddInfo Value
 
-/--
-Suspended values are thunks that return a value. For optimization purposes, the value's
-`TypeInfo`, which by type preservation comes from the underlying expression that gave
-rise to this value by means of evaluation, is saved outside the thunk, instead of in
-the values themselves. This allows us to extract it without needing to force the thunk.
--/
-abbrev SusValue := AddInfo (Thunk Value)
-
 /--
 The environment will bind free variables to different things, depending on
 the evaluation strategy:
@@ -150,30 +152,15 @@ the evaluation strategy:
 2) Non-strict evaluation: binds free variables to unevaluated expressions
 3) Lazy evaluation (i.e. non-strict without duplication of work): binds free variables to thunks
 
-Here we chose lazy evaluation since it is more efficient for typechecking.
+Here we will chose strict evaluation
 
 Since we also have universes with free variables, we need to add a environment
 for universe variables as well
 -/
-abbrev Env := Env' SusValue
+abbrev Env := Env' TypedValue
 
 /-- The arguments of a stuck sequence of applications `(h a1 ... an)` -/
-abbrev Args := List SusValue
-
-instance : Inhabited SusValue where
-  default := .mk default {fn := default}
-
--- Auxiliary functions
-namespace AddInfo
-
-def expr (t : TypedExpr) : Expr := t.body
-def thunk (sus : SusValue) : Thunk Value := sus.body
-def get (sus : SusValue) : Value := sus.body.get
-def getTyped (sus : SusValue) : TypedValue := ⟨sus.info, sus.body.get⟩
-def value (val : TypedValue) : Value := val.body
-def sus (val : TypedValue) : SusValue := ⟨val.info, val.body⟩
-
-end AddInfo
+abbrev Args := List TypedValue
 
 def Value.neu (neu : Neutral) : Value := .app neu [] []
 
@@ -192,11 +179,11 @@ def Neutral.ctorName : Neutral → String
 
 namespace Env'
 /-- Stacks a new expression in the environment -/
-def extendWith (env : Env) (thunk : SusValue) : Env :=
-  .mk (thunk :: env.exprs) env.univs
+def extendWith (env : Env) (val : TypedValue) : Env :=
+  .mk (val :: env.exprs) env.univs
 
 /-- Sets a list of expressions to a environment -/
-def withExprs (env : Env) (exprs : List SusValue) : Env :=
+def withExprs (env : Env) (exprs : List TypedValue) : Env :=
   .mk exprs env.univs
 
 end Env'
@@ -205,9 +192,9 @@ end Env'
 def mkConst (f : F) (univs : List Univ) : Value :=
   .neu (.const f univs)
 
-/-- Creates a new variable as a thunk -/
-def mkSusVar (info : TypeInfo) (idx : Nat) : SusValue :=
-  .mk info (.mk fun _ => .neu (.fvar idx))
+/-- Creates a new variable as a typed value -/
+def mkVar (info : TypeInfo) (idx : Nat) : TypedValue :=
+  .mk info $ .neu (.fvar idx)
 
 inductive PrimConstOp
   | natAdd | natMul | natPow | natBeq | natBle | natBlt  | natSucc
diff --git a/Yatima/Typechecker/Equal.lean b/Yatima/Typechecker/Equal.lean
index 46c63e40..ef05bd27 100644
--- a/Yatima/Typechecker/Equal.lean
+++ b/Yatima/Typechecker/Equal.lean
@@ -26,7 +26,7 @@ Note: Generally the values are assumed to already have the same type in the func
 namespace Yatima.Typechecker
 
 /-- Reduces the application of a `pi` type to its arguments -/
-def applyType : Value → List SusValue → TypecheckM Value
+def applyType : Value → List TypedValue → TypecheckM Value
   | .pi _ img imgCtx, arg :: args => do
     let res ← withEnv (imgCtx.extendWith arg) (eval img)
     applyType res args
@@ -34,8 +34,8 @@ def applyType : Value → List SusValue → TypecheckM Value
   | _, _ => throw "Invalid case for applyType"
 
 mutual
-  partial def tryEtaStruct (lvl : Nat) (term term' : SusValue) : TypecheckM Bool := do
-    match term'.get with
+  partial def tryEtaStruct (lvl : Nat) (term term' : TypedValue) : TypecheckM Bool := do
+    match term'.body with
     | .app (.const k _) args _ =>
       match ← derefTypedConst k with
       | .constructor type .. =>
@@ -45,9 +45,9 @@ mutual
           | .inductive _ struct .. =>
             if struct then
               args.enum.foldlM (init := true) fun acc (i, arg) => do
-                match arg.get with
+                match arg.body with
                 | .app (.proj _ idx val) _ _ =>
-                  pure $ acc && i == idx && (← equal lvl term val.sus)
+                  pure $ acc && i == idx && (← equal lvl term val)
                 | _ => pure false
             else
               pure false
@@ -57,41 +57,39 @@ mutual
     | _ => pure false
 
   /--
-  Checks if two suspended values `term term' : SusValue` at level `lvl : Nat` are equal.
+  Checks if two values `term term' : TypedValue` at level `lvl : Nat` are equal.
 
   It is assumed here that the values are typechecked, have both the same type and their
   original unevaluated terms both lived in the same context.
   -/
-  partial def equal (lvl : Nat) (term term' : SusValue) : TypecheckM Bool :=
+  partial def equal (lvl : Nat) (term term' : TypedValue) : TypecheckM Bool :=
     match term.info, term'.info with
     | .unit, .unit => pure true
     | .proof, .proof => pure true
     | _, _ => do
-      let term! := term.get
-      let term'! := term'.get
-      match term!, term'! with
+      match term.body, term'.body with
       | .lit lit, .lit lit' => pure $ lit == lit'
       | .sort u, .sort u' => pure $ u.equalUniv u'
       | .pi dom img env, .pi dom' img' env' => do
         let res  ← equal lvl dom dom'
-        let img  := suspend img  { ← read with env := env.extendWith  (mkSusVar dom.info  lvl) } (← get)
-        let img' := suspend img' { ← read with env := env'.extendWith (mkSusVar dom'.info lvl) } (← get)
+        let img  ← withNewExtendedEnv env  (mkVar dom.info  lvl) $ evalTyped img
+        let img' ← withNewExtendedEnv env' (mkVar dom'.info lvl) $ evalTyped img'
         let res' ← equal (lvl + 1) img img'
         pure $ res && res'
       | .lam dom bod env, .lam dom' bod' env' => do
         let res  ← equal lvl dom dom'
-        let bod  := suspend bod  { ← read with env := env.extendWith  (mkSusVar dom.info  lvl) } (← get)
-        let bod' := suspend bod' { ← read with env := env'.extendWith (mkSusVar dom'.info lvl) } (← get)
+        let bod  ← withNewExtendedEnv env  (mkVar dom.info  lvl) $ evalTyped bod
+        let bod' ← withNewExtendedEnv env' (mkVar dom'.info lvl) $ evalTyped bod'
         let res' ← equal (lvl + 1) bod bod'
         pure $ res && res'
       | .lam dom bod env, .app neu' args' infos' => do
-        let var := mkSusVar dom.info lvl
-        let bod  := suspend bod { ← read with env := env.extendWith var } (← get)
+        let var := mkVar dom.info lvl
+        let bod  ← withNewExtendedEnv env var $ evalTyped bod
         let app := Value.app neu' (var :: args') (term'.info :: infos')
         equal (lvl + 1) bod (.mk bod.info app)
       | .app neu args infos, .lam dom bod env => do
-        let var := mkSusVar dom.info lvl
-        let bod  := suspend bod { ← read with env := env.extendWith var } (← get)
+        let var := mkVar dom.info lvl
+        let bod  ← withNewExtendedEnv env var $ evalTyped bod
         let app := Value.app neu (var :: args) (term.info :: infos)
         equal (lvl + 1) (.mk bod.info app) bod
       | .app (.fvar idx) args _, .app (.fvar idx') args' _ =>
@@ -99,11 +97,11 @@ mutual
           -- If our assumption is correct, i.e., that these values come from terms
           -- in the same environment then their types are equal when their indices
           -- are equal
-          equalThunks lvl args args'
+          equalValues lvl args args'
         else pure false
       | .app (.const k us) args _, .app (.const k' us') args' _ =>
         if k == k' && IR.Univ.equalUnivs us us' then
-          equalThunks lvl args args'
+          equalValues lvl args args'
         else pure false
       | _, .app (.const _ _) _ _ =>
         tryEtaStruct lvl term term'
@@ -111,9 +109,9 @@ mutual
         tryEtaStruct lvl term' term
       | .app (.proj ind idx val) args _, .app (.proj ind' idx' val') args' _ =>
           if ind == ind' && idx == idx' then do
-            let eqVal ← equal lvl val.sus val'.sus
-            let eqThunks ← equalThunks lvl args args'
-            pure (eqVal && eqThunks)
+            let eqVal ← equal lvl val val'
+            let eqVals ← equalValues lvl args args'
+            pure (eqVal && eqVals)
           else pure false
       | .exception e, _ | _, .exception e =>
         throw s!"exception in equal: {e}"
@@ -121,14 +119,13 @@ mutual
         pure false
 
 /--
-Checks if two list of thunks `vals vals' : List SusValue` are equal by evaluating the thunks
-and checking the evaluated images are equal.
+Checks if two list of values `vals vals' : List TypedValue` are equal
 -/
-  partial def equalThunks (lvl : Nat) (vals vals' : List SusValue) : TypecheckM Bool :=
+  partial def equalValues (lvl : Nat) (vals vals' : List TypedValue) : TypecheckM Bool :=
     match vals, vals' with
     | val::vals, val'::vals' => do
       let eq ← equal lvl val val'
-      let eq' ← equalThunks lvl vals vals'
+      let eq' ← equalValues lvl vals vals'
       pure $ eq && eq'
     | [], [] => pure true
     | _, _ => pure false
diff --git a/Yatima/Typechecker/Eval.lean b/Yatima/Typechecker/Eval.lean
index dd7f9c8f..9c99d3cb 100644
--- a/Yatima/Typechecker/Eval.lean
+++ b/Yatima/Typechecker/Eval.lean
@@ -15,10 +15,7 @@ TODO: Add a high level overview of Eval in the context of Eval-Equal-Infer.
 
 ## Evaluate
 
-In this module the evaluation (↔ reduction) of Yatima expressions is defined. Expressions that can
-be reduced take a few forms, for example `.app fnc args`, constants, and suspdended evaluations.
-Functions that can not be reduced further evaluate to unreduced Values or suspended thunks waiting
-to evaluate further.
+In this module the evaluation (↔ reduction) of Yatima expressions is defined.
 -/
 
 namespace Yatima
@@ -159,31 +156,30 @@ mutual
   evaluating a constant, instantiating a universe variable, evaluating the body of a let binding
   and evaluating a projection.
   -/
-  partial def eval (t : TypedExpr) : TypecheckM Value := match t.expr with
+  partial def eval (t : TypedExpr) : TypecheckM Value := match t.body with
     | .app fnc arg => do
-      let ctx ← read
-      let argThunk := suspend arg ctx (← get)
       let fnc ← evalTyped fnc
-      apply fnc argThunk
+      let arg ← evalTyped arg
+      apply fnc arg
     | .lam dom bod => do
       let ctx ← read
-      let dom' := suspend dom ctx (← get)
-      pure $ .lam dom' bod ctx.env
+      let dom ← evalTyped dom
+      pure $ .lam dom bod ctx.env
     | .var idx => do
-      let some thunk := (← read).env.exprs.get? idx
+      let some value := (← read).env.exprs.get? idx
         | throw s!"Index {idx} is out of range for expression environment"
-      pure $ thunk.get
+      pure $ value.body
     | .const f const_univs => do
       let env := (← read).env
       let const_univs := const_univs.map (Univ.instBulkReduce env.univs)
       evalConst f const_univs
     | .letE _ val bod => do
-      let thunk := suspend val (← read) (← get)
-      withExtendedEnv thunk (eval bod)
+      let val ← evalTyped val
+      withExtendedEnv val (eval bod)
     | .pi dom img => do
       let ctx ← read
-      let dom' := suspend dom ctx (← get)
-      pure $ .pi dom' img ctx.env
+      let dom ← evalTyped dom
+      pure $ .pi dom img ctx.env
     | .sort univ => do
       let env := (← read).env
       pure $ .sort (Univ.instBulkReduce env.univs univ)
@@ -201,7 +197,7 @@ mutual
           let idx := ctor.params + idx
           let some arg := args.reverse.get? idx
             | throw s!"Invalid projection of index {idx} but constructor has only {args.length} arguments"
-          pure $ arg.get
+          pure arg.body
         | _ => pure $ .neu (.proj ind idx (.mk (expr.info.update (← read).env.univs) val))
       | .app .. => pure $ .neu (.proj ind idx (.mk (expr.info.update (← read).env.univs) val))
       | e => throw s!"Value {← ppValue e} is impossible to project"
@@ -231,31 +227,17 @@ mutual
     else evalConst' const univs
 
   /--
-  Suspends the evaluation of a Yatima expression `expr : TypedExpr` in a particular `ctx : TypecheckCtx`
-
-  Suspended evaluations can be resumed by evaluating `Thunk.get` on the resulting Thunk.
-  -/
-  partial def suspend (expr : TypedExpr) (ctx : TypecheckCtx) (stt : TypecheckState) : SusValue :=
-    let thunk := { fn := fun _ =>
-      match TypecheckM.run ctx stt (eval expr) with
-      | .ok a =>
-        a
-      | .error e => .exception e }
-    let reducedInfo := expr.info.update ctx.env.univs
-    ⟨reducedInfo, thunk⟩
-
-  /--
-  Applies `value : Value` to the argument `arg : SusValue`.
+  Applies `value : TypedValue` to the argument `arg : TypedValue`.
 
   Applications are split into cases on whether `value` is a `Value.lam`, the application of a constant
   or the application of a free variable.
 
   * `Value.lam` : Descends into and evaluates the body of the lambda expression
   * `Value.app (.const ..)` : Applies the constant to the argument as expected using `applyConst`
-  * `Value.app (.fvar ..)` : Returns an unevaluated `Value.app`
+  * `Value.app (.fvar ..)` : Returns a `Value.app`
   -/
-  partial def apply (val : TypedValue) (arg : SusValue) : TypecheckM Value :=
-    match val.value with
+  partial def apply (val : TypedValue) (arg : TypedValue) : TypecheckM Value :=
+    match val.body with
     | .lam _ bod lamEnv =>
       withNewExtendedEnv lamEnv arg (eval bod)
     | .app (.const f kUnivs) args infos => applyConst f kUnivs arg args val.info infos
@@ -273,7 +255,7 @@ mutual
   The application of the constant is split into cases on whether it is an inductive recursor,
   a quotient, or any other constant (which returns an unreduced application)
    -/
-  partial def applyConst (f : F) (univs : List Univ) (arg : SusValue) (args : List SusValue)
+  partial def applyConst (f : F) (univs : List Univ) (arg : TypedValue) (args : List TypedValue)
       (info : TypeInfo) (infos : List TypeInfo) : TypecheckM Value := do
     if let some $ .op p ← fPrim f then
       if args.length < p.numArgs - 1 then
@@ -305,7 +287,7 @@ mutual
           throw s!"Too few arguments ({nArgs}). At least {nDrop} needed"
         let minorIdx := nArgs - nDrop
         let some minor := args.get? minorIdx | throw s!"Index {minorIdx} is out of range"
-        pure minor.get
+        pure minor.body
       else
         let params := args.take params
         match ← toCtorIfLitOrStruct indProj params univs arg with
@@ -329,11 +311,11 @@ mutual
   /--
   Applies a quotient to a value. It might reduce if enough arguments are applied to it
   -/
-  partial def applyQuot (major? : SusValue) (args : List SusValue)
+  partial def applyQuot (major? : TypedValue) (args : List TypedValue)
       (reduceSize argPos : Nat) (default : Value) : TypecheckM Value :=
     let argsLength := args.length + 1
     if argsLength == reduceSize then
-      match major?.get with
+      match major?.body with
       | .app (.const majorFn _) majorArgs _ => do
         match ← derefTypedConst majorFn with
         | .quotient _ .ctor =>
@@ -341,7 +323,7 @@ mutual
           if majorArgs.length != 3 then throw "majorArgs should have size 3"
           let some majorArg := majorArgs.head? | throw "majorArgs can't be empty"
           let some head := args.get? argPos | throw s!"{argPos} is an invalid index for args"
-          apply head.getTyped majorArg
+          apply head majorArg
         | _ => pure default
       | _ => pure default
     else if argsLength < reduceSize then
@@ -349,16 +331,16 @@ mutual
     else
       throw s!"argsLength {argsLength} can't be greater than reduceSize {reduceSize}"
 
-  partial def toCtorIfLitOrStruct (indProj : InductiveProj) (params : List SusValue) (univs : List Univ) : SusValue → TypecheckM Value
-    | .mk info thunk =>
-      match thunk.get with
+  partial def toCtorIfLitOrStruct (indProj : InductiveProj) (params : List TypedValue) (univs : List Univ) : TypedValue → TypecheckM Value
+    | .mk info val =>
+      match val with
       | .lit (.natVal v) => do
         let zeroIdx ← primF .natZero
         let succIdx ← primF (.op .natSucc)
         if v == 0 then pure $ mkConst zeroIdx []
         else
-          let thunk : SusValue := ⟨info, Value.lit $ .natVal (v-1)⟩
-          pure $ .app (.const succIdx []) [thunk] [.none]
+          let val := ⟨info, Value.lit $ .natVal (v-1)⟩
+          pure $ .app (.const succIdx []) [val] [.none]
       | .lit (.strVal _) => throw "TODO Reduction of string"
       | e => do
         -- do not eta expand structs in `Prop`
@@ -383,11 +365,10 @@ mutual
                 let f := mkInductiveProjF f i (← read).quick
                 throw s!"{(← read).constNames.getF f} should be a struct with only one constructor"
             let etaExpand (e : Value) : TypecheckM Value := do
-              let mut projArgs : List SusValue := params
+              let mut projArgs : List TypedValue := params
               for idx in [:ctor.fields] do
                 -- FIXME get the correct TypeInfo for the projection
-                projArgs := projArgs ++ [.mk .none $ .mk fun _ =>
-                  .neu (.proj (mkInductiveProjF f i quick) idx $ .mk info e)]
+                projArgs := projArgs ++ [.mk .none $ .neu (.proj (mkInductiveProjF f i quick) idx $ .mk info e)]
               let len := projArgs.length
               if h : len > 0 then
                 let lastIdx := len.pred
@@ -411,24 +392,24 @@ mutual
       if args.tail.length != infos.tail.length then throw "Partial application does not have enough info"
       let argsInfos := args.zip infos
       argsInfos.foldrM (init := ← quoteNeutral lvl env neu) fun (arg, info) acc => do
-        pure $ .app ⟨info, acc⟩ $ ← quoteTyped lvl env arg.getTyped
+        pure $ .app ⟨info, acc⟩ $ ← quoteTyped lvl env arg
     | .lam dom bod env' => do
-      let dom ← quoteTyped lvl env dom.getTyped
+      let dom ← quoteTyped lvl env dom
       -- NOTE: although we add a value with `default` as `TypeInfo`, this is overwritten by the info of the expression's value
-      let var := mkSusVar default lvl
+      let var := mkVar default lvl
       let bod ← quoteTypedExpr (lvl+1) bod (env'.extendWith var)
       pure $ .lam dom bod
     | .pi dom img env' => do
-      let dom ← quoteTyped lvl env dom.getTyped
-      let var := mkSusVar default lvl
+      let dom ← quoteTyped lvl env dom
+      let var := mkVar default lvl
       let img ← quoteTypedExpr (lvl+1) img (env'.extendWith var)
       pure $ .pi dom img
     | .lit lit => pure $ .lit lit
-    | .exception e => throw e
+    | .exception e => throw s!"{e}"
 
   @[inline]
   partial def quoteTyped (lvl : Nat) (env : Env) (val : TypedValue) : TypecheckM TypedExpr := do
-    pure ⟨val.info, ← quote lvl env val.value⟩
+    pure ⟨val.info, ← quote lvl env val.body⟩
 
   partial def quoteExpr (lvl : Nat) (expr : Expr) (env : Env) : TypecheckM Expr :=
     match expr with
@@ -437,7 +418,7 @@ mutual
       -- NOTE: if everything is correct, then `info` should coincide with `val.info`. We will choose `info` since
       -- this allows us to add values to the environment without knowing which `TypeInfo` it should take. See their
       -- previous note
-     | some val => quote lvl env val.get
+     | some val => quote lvl env val.body
      | none => throw s!"Unbound variable _@{idx}"
     | .app fnc arg => do
       let fnc ← quoteTypedExpr lvl fnc env
@@ -445,18 +426,18 @@ mutual
       pure $ .app fnc arg
     | .lam dom bod => do
       let dom ← quoteTypedExpr lvl dom env
-      let var := mkSusVar default lvl
+      let var := mkVar default lvl
       let bod ← quoteTypedExpr (lvl+1) bod (env.extendWith var)
       pure $ .lam dom bod
     | .letE typ val bod => do
       let typ ← quoteTypedExpr lvl typ env
       let val ← quoteTypedExpr lvl val env
-      let var := mkSusVar default lvl
+      let var := mkVar default lvl
       let bod ← quoteTypedExpr (lvl+1) bod (env.extendWith var)
       pure $ .letE typ val bod
     | .pi dom img => do
       let dom ← quoteTypedExpr lvl dom env
-      let var := mkSusVar default lvl
+      let var := mkVar default lvl
       let img ← quoteTypedExpr (lvl+1) img (env.extendWith var)
       pure $ .pi dom img
     | .proj ind idx expr => do
@@ -468,7 +449,7 @@ mutual
 
   @[inline]
   partial def quoteTypedExpr (lvl : Nat) (t : TypedExpr) (env : Env) : TypecheckM TypedExpr := do
-    pure ⟨t.info, ← quoteExpr lvl t.expr env⟩
+    pure ⟨t.info, ← quoteExpr lvl t.body env⟩
 
   partial def quoteNeutral (lvl : Nat) (env : Env) : Neutral → TypecheckM Expr
     | .fvar  idx => pure $ .var (lvl - idx - 1)
diff --git a/Yatima/Typechecker/Infer.lean b/Yatima/Typechecker/Infer.lean
index dd7eb50c..43612e84 100644
--- a/Yatima/Typechecker/Infer.lean
+++ b/Yatima/Typechecker/Infer.lean
@@ -36,20 +36,20 @@ def piInfo (dom img : TypeInfo) : TypecheckM TypeInfo := match dom, img with
 | _, .sort _ => throw "Domain is not a type"
 | _, _ => throw "Neither image nor domain are types"
 
-def eqSortInfo (inferType expectType : SusValue) : TypecheckM Bool := do
+def eqSortInfo (inferType expectType : TypedValue) : TypecheckM Bool := do
   match inferType.info, expectType.info with
   | .sort lvl, .sort lvl' => pure $ lvl.equalUniv lvl'
-  | .sort _, e => throw s!"Expected type {← ppValue expectType.get} {repr e} is not actually a type"
-  | e, .sort _ => throw s!"Inferred type {← ppValue inferType.get} {repr e} is not actually a type"
-  | e, e' => throw s!"Neither expected {← ppValue expectType.get} {repr e} nor inferred types {← ppValue inferType.get} {repr e'} are actually types"
+  | .sort _, e => throw s!"Expected type {← ppValue expectType.body} {repr e} is not actually a type"
+  | e, .sort _ => throw s!"Inferred type {← ppValue inferType.body} {repr e} is not actually a type"
+  | e, e' => throw s!"Neither expected {← ppValue expectType.body} {repr e} nor inferred types {← ppValue inferType.body} {repr e'} are actually types"
 /--
   Gives the correct type information for a term based on its type.
 -/
-def infoFromType (typ : SusValue) : TypecheckM TypeInfo :=
+def infoFromType (typ : TypedValue) : TypecheckM TypeInfo :=
   match typ.info with
   | .sort .zero => pure .proof
   | _ =>
-    match typ.get with
+    match typ.body with
     | .app (.const f _) _ _ => do match derefConst f (← read).store with
       | .inductiveProj p =>
         let induct ← getIndFromProj p
@@ -61,7 +61,7 @@ def infoFromType (typ : SusValue) : TypecheckM TypeInfo :=
 mutual
 
   partial def getStructInfo (v : Value) :
-      TypecheckM (F × TypedExpr × List Univ × List SusValue) := do
+      TypecheckM (F × TypedExpr × List Univ × List TypedValue) := do
     match v with
     | .app (.const indF univs) params _ =>
       let .inductiveProj p := derefConst indF (← read).store 
@@ -79,18 +79,18 @@ mutual
     | v => throw s!"Expected a structure type, found {← ppValue v}"
 
   /--
-  Checks if `term : IR.Expr` has type `type : SusValue`. Returns the typed IR for `term`
+  Checks if `term : IR.Expr` has type `type : TypedValue`. Returns the typed IR for `term`
   -/
-  partial def check (term : IR.Expr) (type : SusValue) : TypecheckM TypedExpr := do
+  partial def check (term : IR.Expr) (type : TypedValue) : TypecheckM TypedExpr := do
     let (term, inferType) ← infer term
     if !(← eqSortInfo inferType type) then
-      throw s!"Term: {← ppTypedExpr term}\nInfo mismatch:\n{repr inferType.info}\n\nnot equal to\n{repr type.info}\n\nExpected type: {← ppValue type.get}\nInferred type: {← ppValue inferType.get}"
+      throw s!"Term: {← ppTypedExpr term}\nInfo mismatch:\n{repr inferType.info}\n\nnot equal to\n{repr type.info}\n\nExpected type: {← ppValue type.body}\nInferred type: {← ppValue inferType.body}"
     if !(← equal (← read).lvl type inferType) then
-      throw s!"Expected type {← ppValue type.get}, found type {← ppValue inferType.get}"
+      throw s!"Expected type {← ppValue type.body}, found type {← ppValue inferType.body}"
     pure term
 
   /-- Infers the type of `term : IR.Expr`. Returns the typed IR for `term` along with its inferred type  -/
-  partial def infer (term : IR.Expr) : TypecheckM (TypedExpr × SusValue) := do
+  partial def infer (term : IR.Expr) : TypecheckM (TypedExpr × TypedValue) := do
     match term with
     | .var idx lvls =>
       let ctx ← read
@@ -107,12 +107,12 @@ mutual
       else
         -- this free variable came from `recrCtx`, and thus represents a mutual reference
         match ctx.mutTypes.find? (idx - ctx.lvl) with
-        | some (constF, typeValFn) =>
+        | some (constF, exprs, type) =>
           if some constF == ctx.recF? then
             throw s!"Invalid recursion in {(← read).constNames.getF constF}"
-          let type := typeValFn lvls
-          let term := ⟨← infoFromType type, .const constF lvls⟩
-          pure (term, type)
+          let typeVal ← withEnv ⟨exprs, lvls⟩ $ evalTyped type
+          let term := ⟨← infoFromType typeVal, .const constF lvls⟩
+          pure (term, typeVal)
         | none =>
           throw $ s!"var@{idx} out of environment range (size {ctx.types.length})"
             ++ " and does not represent a mutual constant"
@@ -120,49 +120,47 @@ mutual
       let univs := (← read).env.univs
       let lvl := Univ.instBulkReduce univs lvl
       let lvl' := lvl.succ
-      let typ := .mk (.sort lvl'.succ) ⟨ fun _ => .sort lvl' ⟩
+      let typ := .mk (.sort lvl'.succ) (.sort lvl')
       -- NOTE: we populate `SusTypeInfo.sort` here for consistency but technically it isn't necessary
       -- because `lvl'` can never become `Univ.zero`.
       let term := ⟨.sort lvl', .sort lvl⟩
       return (term, typ)
     | .app fnc' arg =>
       let (fnc, fncType) ← infer fnc'
-      match fncType.get with
+      match fncType.body with
       | .pi dom img env =>
         let arg ← check arg dom
-        let ctx ← read
-        let stt ← get
-        let typ := suspend img { ctx with env := env.extendWith $ suspend arg ctx stt} stt
+        let argVal ← evalTyped arg
+        let typ ← withNewExtendedEnv env argVal $ evalTyped img
         let term := ⟨← infoFromType typ, .app fnc arg⟩
         pure (term, typ)
       | val => throw s!"Expected a pi type, found {← ppValue val}"
     | .lam dom bod => do
       let (dom, _) ← isSort dom
       let ctx ← read
-      let domVal := suspend dom ctx (← get)
-      let var := mkSusVar (← infoFromType domVal) ctx.lvl
+      let domVal ← evalTyped dom
+      let var := mkVar (← infoFromType domVal) ctx.lvl
       let (bod, imgVal) ← withExtendedCtx var domVal $ infer bod
       let term := ⟨lamInfo bod.info, .lam dom bod⟩
       let typ := .mk (← piInfo domVal.info imgVal.info) $
-        Value.pi domVal (← quoteTyped (ctx.lvl+1) ctx.env imgVal.getTyped) ctx.env
+        Value.pi domVal (← quoteTyped (ctx.lvl+1) ctx.env imgVal) ctx.env
       pure (term, typ)
     | .pi dom img =>
       let (dom, domLvl) ← isSort dom
       let ctx ← read
-      let domVal := suspend dom ctx (← get)
-      let domSusVal := mkSusVar (← infoFromType domVal) ctx.lvl
+      let domVal ← evalTyped dom
+      let domSusVal := mkVar (← infoFromType domVal) ctx.lvl
       withExtendedCtx domSusVal domVal $ do
         let (img, imgLvl) ← isSort img
         let sortLvl := .reduceIMax domLvl imgLvl
-        let typ := .mk (.sort sortLvl.succ) ⟨ fun _ => .sort $ sortLvl ⟩
+        let typ := .mk (.sort sortLvl.succ) (.sort $ sortLvl)
         let term := ⟨← infoFromType typ, .pi dom img⟩
         return (term, typ)
     | .letE expType exp bod =>
       let (expType, _) ← isSort expType
-      let ctx ← read
-      let expTypeVal := suspend expType ctx (← get)
+      let expTypeVal ← evalTyped expType
       let exp ← check exp expTypeVal
-      let expVal := suspend exp ctx (← get)
+      let expVal ← evalTyped exp
       let (bod, typ) ← withExtendedCtx expVal expTypeVal $ infer bod
       let term := ⟨bod.info, .letE expType exp bod⟩
       return (term, typ)
@@ -180,18 +178,18 @@ mutual
       let univs := ctx.env.univs
       let tconst ← derefTypedConst k
       let env := ⟨[], constUnivs.map (Univ.instBulkReduce univs)⟩
-      let typ := suspend tconst.type { ctx with env := env } (← get)
+      let typ ← withEnv env $ evalTyped tconst.type
       let term := ⟨← infoFromType typ, .const k constUnivs⟩
       pure (term, typ)
     | .proj idx expr =>
       let (expr, exprType) ← infer expr
-      let (indF, ctorType, univs, params) ←  getStructInfo exprType.get
+      let (indF, ctorType, univs, params) ←  getStructInfo exprType.body
       let mut ctorType ← applyType (← withEnv ⟨[], univs⟩ $ eval ctorType) params.reverse
       for i in [:idx] do
         match ctorType with
         | .pi dom img piEnv =>
           let info ← infoFromType dom
-          let proj := suspend ⟨info, .proj indF i expr⟩ (← read) (← get)
+          let proj ← evalTyped ⟨info, .proj indF i expr⟩
           ctorType ← withNewExtendedEnv piEnv proj $ eval img
         | _ => pure ()
       match ctorType with
@@ -213,7 +211,7 @@ mutual
   -/
   partial def isSort (expr : IR.Expr) : TypecheckM (TypedExpr × Univ) := do
     let (expr, typ) ← infer expr
-    match typ.get with
+    match typ.body with
     | .sort u =>
       pure (expr, u)
     | val => throw s!"Expected a sort type, found {← ppValue val}"
@@ -225,15 +223,13 @@ mutual
       | _ => throw "Invalid Const kind. Expected mutIndBlock"
 
     -- Check all inductives
-    let mut mutTypes := .empty
+    let mut mutTypes : RecrCtx := .empty
     for (indIdx, ind) in indBlock.enum do
       let f := mkInductiveProjF indBlockF indIdx quick
       let univs := List.range ind.lvls |>.map .var
       let (type, _) ← withEnv ⟨ [], univs ⟩ $ isSort ind.type
       let ctx ← read
-      let stt ← get
-      let typeSus := (suspend type {ctx with env := .mk ctx.env.exprs ·} stt)
-      mutTypes := mutTypes.insert indIdx (f, typeSus)
+      mutTypes := mutTypes.insert indIdx (f, ctx.env.exprs, type)
       modify fun stt => { stt with typedConsts := stt.typedConsts.insert f (.inductive type ind.struct) }
 
     -- Check all constructors
@@ -244,9 +240,7 @@ mutual
         let univs := List.range ctor.lvls |>.map .var
         let (type, _) ← withEnv ⟨ [], univs ⟩ $ withMutTypes mutTypes $ isSort ctor.type
         let ctx ← read
-        let stt ← get
-        let typeSus := (suspend type {ctx with env := .mk ctx.env.exprs ·} stt)
-        mutTypes := mutTypes.insert (start + cidx) (f, typeSus)
+        mutTypes := mutTypes.insert (start + cidx) (f, ctx.env.exprs, type)
         modify fun stt => { stt with typedConsts := stt.typedConsts.insert f (.constructor type ctor.idx ctor.fields) }
 
     -- Check all recursor types
@@ -257,9 +251,7 @@ mutual
         let univs := List.range recr.lvls |>.map .var
         let (type, _) ← withEnv ⟨ [], univs ⟩ $ withMutTypes mutTypes $ isSort recr.type
         let ctx ← read
-        let stt ← get
-        let typeSus := (suspend type {ctx with env := .mk ctx.env.exprs ·} stt)
-        mutTypes := mutTypes.insert (start + ridx) (f, typeSus)
+        mutTypes := mutTypes.insert (start + ridx) (f, ctx.env.exprs, type)
 
     -- Check all recursor rules
     for (indIdx, ind) in indBlock.enum do
@@ -306,25 +298,24 @@ mutual
             pure $ TypedConst.axiom type
           | .opaque data =>
             let (type, _) ← isSort data.type
-            let typeSus := suspend type (← read) (← get)
-            let value ← withRecF f $ check data.value typeSus
+            let typeVal ← evalTyped type
+            let value ← withRecF f $ check data.value typeVal
             pure $ TypedConst.opaque type value
           | .theorem data =>
             let (type, _) ← isSort data.type
-            let typeSus := suspend type (← read) (← get)
-            let value ← withRecF f $ check data.value typeSus
+            let typeVal ← evalTyped type
+            let value ← withRecF f $ check data.value typeVal
             pure $ TypedConst.theorem type value
           | .definition data =>
             let (type, _) ← isSort data.type
             let ctx ← read
-            let typeSus := suspend type ctx (← get)
+            let typeVal ← evalTyped type
             let value ←
               if data.part then
                 let mutTypes :=
-                  let typeSus := (suspend type {ctx with env := .mk ctx.env.exprs ·} (← get))
-                  (default : RecrCtx).insert 0 (f, typeSus)
-                withMutTypes mutTypes $ withRecF f $ check data.value typeSus
-              else withRecF f $ check data.value typeSus
+                  (default : RecrCtx).insert 0 (f, ctx.env.exprs, type)
+                withMutTypes mutTypes $ withRecF f $ check data.value typeVal
+              else withRecF f $ check data.value typeVal
             pure $ TypedConst.definition type value data.part
           | .definitionProj p@⟨defBlockF, _⟩ =>
             let data ← getDefFromProj p
@@ -333,7 +324,7 @@ mutual
             let defBlock ← match derefConst defBlockF ctx.store with
               | .mutDefBlock blk => pure blk
               | _ => throw "Invalid Const kind. Expected mutDefBlock"
-            let typeSus := suspend type ctx (← get)
+            let typeVal ← evalTyped type
             let value ←
               if data.part then
                 -- check order should be the same as `recrCtx` in CA
@@ -341,10 +332,9 @@ mutual
                   let defProjF := mkDefinitionProjF defBlockF i quick
                   -- TODO avoid repeated work here
                   let (type, _) ← isSort defn.type
-                  let typeSus := (suspend type {ctx with env := .mk ctx.env.exprs ·} (← get))
-                  pure $ acc.insert i (defProjF, typeSus)
-                withMutTypes mutTypes $ withRecF f $ check data.value typeSus
-              else withRecF f $ check data.value typeSus
+                  pure $ acc.insert i (defProjF, ctx.env.exprs, type)
+                withMutTypes mutTypes $ withRecF f $ check data.value typeVal
+              else withRecF f $ check data.value typeVal
             pure $ TypedConst.definition type value data.part
           | .inductiveProj ⟨indBlockF, _⟩ =>
             checkIndBlock indBlockF
diff --git a/Yatima/Typechecker/Printing.lean b/Yatima/Typechecker/Printing.lean
index 914e87fd..166100d9 100644
--- a/Yatima/Typechecker/Printing.lean
+++ b/Yatima/Typechecker/Printing.lean
@@ -172,7 +172,7 @@ open IR PP Lean Std.Format
 
 private abbrev indentD := Std.Format.indentD
 
-def TypedExpr.isProp (t : TypedExpr) : Bool := match t.expr with
+def TypedExpr.isProp (t : TypedExpr) : Bool := match t.body with
   | .sort .zero => true
   | _ => false
 
@@ -192,12 +192,12 @@ mutual
     else return f!"({← ppTypedExpr e})"
 
   /-- Printer of expressions -/
-  partial def ppTypedExpr (t : TypedExpr) : TypecheckM Format := match t.expr with
+  partial def ppTypedExpr (t : TypedExpr) : TypecheckM Format := match t.body with
     | .var idx => return f!"v_{idx}"
     | .sort u => return f!"Sort {ppUniv u}"
     | .const k univs =>
       return f!"{(← read).constNames.getF k}@{ppUnivs univs}"
-    | .app fnc arg => match fnc.expr with
+    | .app fnc arg => match fnc.body with
       | .app .. => return f!"{← ppTypedExpr fnc} {← paren arg}"
       | _ => return f!"{← paren fnc} {← paren arg}"
     | .lam dom bod =>
@@ -218,15 +218,15 @@ mutual
 
   /-- Auxiliary function to print the body of a lambda expression given `env : Env` -/
   private partial def ppTypedExprWith (t : TypedExpr) (env : Env) : TypecheckM Format :=
-    match t.expr with
+    match t.body with
     | .var 0 => return f!"v_0"
     | .var (idx + 1) =>
       match env.exprs.get? idx with
-     | some val => ppValue val.get
+     | some val => ppValue val.body
      | none => return f!"!_@{idx}!"
     | .sort u => return f!"Sort {ppUniv u}"
     | .const k univs => return f!"{(← read).constNames.getF k}@{ppUnivs univs}"
-    | .app fnc arg => match fnc.expr with
+    | .app fnc arg => match fnc.body with
       | .app .. => return f!"{← ppTypedExprWith fnc env} {← parenWith arg env}"
       | _ => return f!"{← parenWith fnc env} {← parenWith arg env}"
     -- | .app _ fnc arg => f!"({← ppTypedExprWith fnc env} {← ppTypedExprWith arg env})"
@@ -242,11 +242,11 @@ mutual
   private partial def ppNeutral (neu : Neutral) : TypecheckM Format := match neu with
     | .fvar idx .. => return f!"fv_{idx}"
     | .const k univs => return f!"{(← read).constNames.getF k}@{ppUnivs univs}"
-    | .proj _ idx val => return f!"{← ppValue val.value}.{idx}"
+    | .proj _ idx val => return f!"{← ppValue val.body}.{idx}"
 
   /-- Auxiliary function to print a chain of unevaluated applications as a single application -/
   private partial def ppSpine (neu : Neutral) (args : Args) : TypecheckM Format := do
-    List.foldrM (fun arg str => return f!"{str} {← ppValue arg.get}") (← ppNeutral neu) args
+    List.foldrM (fun arg str => return f!"{str} {← ppValue arg.body}") (← ppNeutral neu) args
 
   /-- Printer of typechecker values -/
   partial def ppValue (val : Value) : TypecheckM Format :=
@@ -254,9 +254,9 @@ mutual
     | .sort u => return f!"Sort {ppUniv u}"
     | .app neu args _ => ppSpine neu args
     | .lam dom bod ctx =>
-      return f!"fun (_ : {← ppValue dom.get}) =>{indentD (← ppTypedExprWith bod ctx)}"
+      return f!"fun (_ : {← ppValue dom.body}) =>{indentD (← ppTypedExprWith bod ctx)}"
     | .pi dom cod ctx =>
-      return f!"(_ : {← ppValue dom.get}) → {← ppTypedExprWith cod ctx}"
+      return f!"(_ : {← ppValue dom.body}) → {← ppTypedExprWith cod ctx}"
     | .lit (.natVal x) => return f!"{x}"
     | .lit (.strVal x) => return f!"\"{x}\""
     | .exception e => return f!"exception {e}"
@@ -271,10 +271,10 @@ def ppTypecheckCtx : TypecheckM Format := do
   let ⟨lvl, env, types, _, _, _, _, _, _, _⟩ ← read
   let env := ← match env with
     | .mk vals us => do
-      let vals : List Value := vals.map (·.get)
+      let vals : List Value := vals.map (·.body)
       let fields := f!"vals := {← vals.mapM ppValue}" ++ line ++ f!"us := {us.map ppUniv}"
       return f!"env with{indentD fields}"
-  let types ← types.mapM fun t => ppValue t.get
+  let types ← types.mapM fun t => ppValue t.body
   let fields := f!"lvl := {lvl}" ++ line ++ f!"env := {env}" ++ line ++ f!"types := {types}"
   return f!"typecheckCtx with{indentD fields}"
 
diff --git a/Yatima/Typechecker/TypecheckM.lean b/Yatima/Typechecker/TypecheckM.lean
index 3f244f99..e40e9616 100644
--- a/Yatima/Typechecker/TypecheckM.lean
+++ b/Yatima/Typechecker/TypecheckM.lean
@@ -13,7 +13,7 @@ namespace Yatima.Typechecker
 open IR
 open Lurk (F)
 
-abbrev RecrCtx    := Std.RBMap Nat (F × (List Univ → SusValue)) compare
+abbrev RecrCtx    := Std.RBMap Nat (F × List TypedValue × TypedExpr) compare
 abbrev ConstNames := Std.RBMap F Lean.Name compare
 abbrev Store      := Std.RBMap F Const compare
 
@@ -21,17 +21,17 @@ abbrev Store      := Std.RBMap F Const compare
 The context available to the typechecker monad. The available fields are
 * `lvl : Nat` : Depth of the subterm. Coincides with the length of the list of types
 * `env : Env` : A environment of known values, and universe levels. See `Env`
-* `types : List SusValue` : The types of the values in `Env`.
+* `types : List TypedValue` : The types of the values in `Env`.
 * `store : Store` : An store of known constants in the context.
 -/
 structure TypecheckCtx where
   lvl         : Nat
   env         : Env
-  types       : List SusValue
+  types       : List TypedValue
   store       : Store
   /-- Maps a variable index (which represents a reference to a mutual const)
     to the hash of that constant (in `TypecheckState.typedConsts`) and
-    a function returning a `SusValue` for that constant's type given a list of universes. -/
+    a function returning a `TypedValue` for that constant's type given a list of universes. -/
   mutTypes    : RecrCtx
   constNames  : ConstNames
   limitAxioms : Bool
@@ -89,12 +89,12 @@ def withMutTypes (mutTypes : RecrCtx) :
 
 /--
 Evaluates a `TypecheckM` computation with a `TypecheckCtx` which has been extended with an additional
-`val : SusValue`, `typ : SusValue` pair.
+`val : TypedValue`, `typ : TypedValue` pair.
 
 The `lvl` of the `TypecheckCtx` is also incremented.
 TODO: Get clarification on this.
 -/
-def withExtendedCtx (val typ : SusValue) : TypecheckM α → TypecheckM α :=
+def withExtendedCtx (val typ : TypedValue) : TypecheckM α → TypecheckM α :=
   withReader fun ctx => { ctx with
     lvl := ctx.lvl + 1,
     types := typ :: ctx.types,
@@ -102,18 +102,18 @@ def withExtendedCtx (val typ : SusValue) : TypecheckM α → TypecheckM α :=
 
 /--
 Evaluates a `TypecheckM` computation with a `TypecheckCtx` with a the environment extended by a
-`thunk : SusValue` (whose type is not known, unlike `withExtendedCtx`)
+`val : TypedValue` (whose type is not known, unlike `withExtendedCtx`)
 -/
-def withExtendedEnv (thunk : SusValue) : TypecheckM α → TypecheckM α :=
-  withReader fun ctx => { ctx with env := ctx.env.extendWith thunk }
+def withExtendedEnv (val : TypedValue) : TypecheckM α → TypecheckM α :=
+  withReader fun ctx => { ctx with env := ctx.env.extendWith val }
 
 /--
 Evaluates a `TypecheckM` computation with a `TypecheckCtx` whose environment is an extension of `env`
-by a `thunk : SusValue` (whose type is not known)
+by a `val : TypedValue`
 -/
-def withNewExtendedEnv (env : Env) (thunk : SusValue) :
+def withNewExtendedEnv (env : Env) (val : TypedValue) :
     TypecheckM α → TypecheckM α :=
-  withReader fun ctx => { ctx with env := env.extendWith thunk }
+  withReader fun ctx => { ctx with env := env.extendWith val }
 
 def withLimitedAxioms : TypecheckM α → TypecheckM α :=
   withReader fun ctx => { ctx with limitAxioms := true }
@@ -121,10 +121,6 @@ def withLimitedAxioms : TypecheckM α → TypecheckM α :=
 def withRecF (f : F) : TypecheckM α → TypecheckM α :=
   withReader fun ctx => { ctx with recF? := some f }
 
-/--
-Evaluates a `TypecheckM` computation with a `TypecheckCtx` whose environment is an extension of `env`
-by a `thunk : SusValue` (whose type is not known)
--/
 def withDbg : TypecheckM α → TypecheckM α :=
   withReader fun ctx => { ctx with dbg := true }
 
@@ -220,37 +216,37 @@ def fPrim (f : F) : TypecheckM $ Option PrimConst := do
   else pure $ fToPrimQuick f
 
 structure PrimOp where
-  op : Array SusValue → TypecheckM (Option Value)
+  op : Array TypedValue → TypecheckM (Option Value)
 
 def PrimConstOp.toPrimOp : PrimConstOp → PrimOp
   | .natSucc => .mk fun vs => do
     let some v := vs.get? 0
-      | throw "At least one SusValue element needed for PrimConstOp.natSucc"
-    match v.get with
+      | throw "At least one TypedValue element needed for PrimConstOp.natSucc"
+    match v.body with
     | .lit (.natVal v) => pure $ .some $ .lit (.natVal v.succ)
     | _ => pure none
   | .natAdd => .mk fun vs => do
     let some (v, v') := do pure (← vs.get? 0, ← vs.get? 1)
-      | throw "At least two SusValue elements needed for PrimConstOp.natAdd"
-    match v.get, v'.get with
+      | throw "At least two TypedValue elements needed for PrimConstOp.natAdd"
+    match v.body, v'.body with
     | .lit (.natVal v), .lit (.natVal v') => pure $ .some $ .lit (.natVal (v+v'))
     | _, _ => pure none
   | .natMul => .mk fun vs => do
     let some (v, v') := do pure (← vs.get? 0, ← vs.get? 1)
-      | throw "At least two SusValue elements needed for PrimConstOp.natMul"
-    match v.get, v'.get with
+      | throw "At least two TypedValue elements needed for PrimConstOp.natMul"
+    match v.body, v'.body with
     | .lit (.natVal v), .lit (.natVal v') => pure $ .some $ .lit (.natVal (v*v'))
     | _, _ => pure none
   | .natPow => .mk fun vs => do
     let some (v, v') := do pure (← vs.get? 0, ← vs.get? 1)
-      | throw "At least two SusValue elements needed for PrimConstOp.natPow"
-    match v.get, v'.get with
+      | throw "At least two TypedValue elements needed for PrimConstOp.natPow"
+    match v.body, v'.body with
     | .lit (.natVal v), .lit (.natVal v') => pure $ .some $ .lit (.natVal (Nat.pow v v'))
     | _, _ => pure none
   | .natBeq => .mk fun vs => do
     let some (v, v') := do pure (← vs.get? 0, ← vs.get? 1)
-      | throw "At least two SusValue elements needed for PrimConstOp.natBeq"
-    match v.get, v'.get with
+      | throw "At least two TypedValue elements needed for PrimConstOp.natBeq"
+    match v.body, v'.body with
     | .lit (.natVal v), .lit (.natVal v') =>
       if v = v' then do
         pure $ some $ .neu (.const (← primF .boolTrue) [])
@@ -259,8 +255,8 @@ def PrimConstOp.toPrimOp : PrimConstOp → PrimOp
     | _, _ => pure none
   | .natBle => .mk fun vs => do
     let some (v, v') := do pure (← vs.get? 0, ← vs.get? 1)
-      | throw "At least two SusValue elements needed for PrimConstOp.natBle"
-    match v.get, v'.get with
+      | throw "At least two TypedValue elements needed for PrimConstOp.natBle"
+    match v.body, v'.body with
     | .lit (.natVal v), .lit (.natVal v') =>
       if v ≤ v' then do
         pure $ some $ .neu (.const (← primF .boolTrue) [])
@@ -269,8 +265,8 @@ def PrimConstOp.toPrimOp : PrimConstOp → PrimOp
     | _, _ => pure none
   | .natBlt => .mk fun vs => do
     let some (v, v') := do pure (← vs.get? 0, ← vs.get? 1)
-      | throw "At least two SusValue elements needed for PrimConstOp.natBlt"
-    match v.get, v'.get with
+      | throw "At least two TypedValue elements needed for PrimConstOp.natBlt"
+    match v.body, v'.body with
     | .lit (.natVal v), .lit (.natVal v') =>
       if v < v' then do
         pure $ some $ .neu (.const (← primF .boolTrue) [])