diff --git a/src/Juvix/Compiler/Core/Extra/Base.hs b/src/Juvix/Compiler/Core/Extra/Base.hs
index 218411abf4..aa10b6e6a5 100644
--- a/src/Juvix/Compiler/Core/Extra/Base.hs
+++ b/src/Juvix/Compiler/Core/Extra/Base.hs
@@ -2,9 +2,8 @@ module Juvix.Compiler.Core.Extra.Base where
 
 import Data.Functor.Identity
 import Data.List qualified as List
-import Data.List.NonEmpty (fromList)
+import Data.List.NonEmpty qualified as NonEmpty
 import Juvix.Compiler.Core.Info qualified as Info
-import Juvix.Compiler.Core.Info.BinderInfo
 import Juvix.Compiler.Core.Language
 
 {------------------------------------------------------------------------}
@@ -46,23 +45,23 @@ mkConstr i tag args = NCtr (Constr i tag args)
 mkConstr' :: Tag -> [Node] -> Node
 mkConstr' = mkConstr Info.empty
 
-mkLambda :: Info -> Node -> Node
-mkLambda i b = NLam (Lambda i b)
+mkLambda :: Info -> Binder -> Node -> Node
+mkLambda i bi b = NLam (Lambda i bi b)
 
 mkLambda' :: Node -> Node
-mkLambda' = mkLambda Info.empty
+mkLambda' = mkLambda Info.empty emptyBinder
 
-mkLet :: Info -> Node -> Node -> Node
-mkLet i v b = NLet (Let i v b)
+mkLet :: Info -> Binder -> Node -> Node -> Node
+mkLet i bi v b = NLet (Let i bi v b)
 
 mkLet' :: Node -> Node -> Node
-mkLet' = mkLet Info.empty
+mkLet' = mkLet Info.empty emptyBinder
 
-mkLetRec :: Info -> NonEmpty Node -> Node -> Node
+mkLetRec :: Info -> NonEmpty (Binder, Node) -> Node -> Node
 mkLetRec i vs b = NRec (LetRec i vs b)
 
 mkLetRec' :: NonEmpty Node -> Node -> Node
-mkLetRec' = mkLetRec Info.empty
+mkLetRec' = mkLetRec Info.empty . NonEmpty.zip (NonEmpty.repeat emptyBinder)
 
 mkCase :: Info -> Node -> [CaseBranch] -> Maybe Node -> Node
 mkCase i v bs def = NCase (Case i v bs def)
@@ -212,9 +211,9 @@ mkLambdas' k
 unfoldLambdasRev :: Node -> ([Info], Node)
 unfoldLambdasRev = go []
   where
-    go :: [Info] -> Node -> ([Info], Node)
+    go :: [LambdaLhs] -> Node -> ([LambdaLhs], Node)
     go acc n = case n of
-      NLam (Lambda i b) -> go (i : acc) b
+      NLam (Lambda i bi b) -> go (LambdaLhs i bi : acc) b
       _ -> (acc, n)
 
 unfoldLambdas :: Node -> ([Info], Node)
@@ -226,29 +225,23 @@ unfoldLambdas' = first length . unfoldLambdas
 {------------------------------------------------------------------------}
 {- functions on Pattern -}
 
-getBinderPatternInfos :: Pattern -> [Info]
+getBinderPatternInfos :: Pattern -> [Binder]
 getBinderPatternInfos = go []
   where
-    go :: [Info] -> Pattern -> [Info]
+    go :: [Binder] -> Pattern -> [Binder]
     go acc = \case
-      PatConstr (PatternConstr {..}) ->
-        foldl' go acc _patternConstrArgs
-      PatBinder (PatternBinder {..}) ->
-        go (_patternBinderInfo : acc) _patternBinderPattern
-      PatWildcard {} ->
-        acc
+      PatConstr PatternConstr {..} -> foldl' go acc _patternConstrArgs
+      PatBinder p -> go (p ^. patternBinder : acc) (p ^. patternBinderPattern)
+      PatWildcard {} -> acc
 
 getPatternInfos :: Pattern -> [Info]
 getPatternInfos = go []
   where
     go :: [Info] -> Pattern -> [Info]
     go acc = \case
-      PatConstr (PatternConstr {..}) ->
-        foldl' go (_patternConstrInfo : acc) _patternConstrArgs
-      PatBinder (PatternBinder {..}) ->
-        go (_patternBinderInfo : acc) _patternBinderPattern
-      PatWildcard (PatternWildcard {..}) ->
-        _patternWildcardInfo : acc
+      PatConstr PatternConstr {..} -> foldl' go (_patternConstrInfo : acc) _patternConstrArgs
+      PatBinder PatternBinder {..} -> go (_patternBinderInfo : acc) _patternBinderPattern
+      PatWildcard PatternWildcard {..} -> _patternWildcardInfo : acc
 
 {------------------------------------------------------------------------}
 {- generic Node destruction -}
@@ -270,11 +263,12 @@ data NodeDetails = NodeDetails
     _nodeChildBindersNum :: [Int],
     -- | 'nodeChildBindersInfo' is information about binders for each child, if
     -- present. Same length and order as in `nodeChildren`.
-    _nodeChildBindersInfo :: [[Info]],
+    _nodeChildBindersInfo :: [[Binder]],
     -- | 'nodeReassemble' reassembles the node from the info, the subinfos and
     -- the children (which should be in the same fixed order as in the
     -- 'nodeSubinfos' and 'nodeChildren' component).
-    _nodeReassemble :: Info -> [Info] -> [Node] -> Node
+    -- TODO can we zip the lists?
+    _nodeReassemble :: Info -> [Info] -> [Binder] -> [Node] -> Node
   }
 
 makeLenses ''NodeDetails
@@ -290,7 +284,7 @@ destruct = \case
         _nodeChildren = [],
         _nodeChildBindersNum = [],
         _nodeChildBindersInfo = [],
-        _nodeReassemble = \i' _ _ -> mkVar i' idx
+        _nodeReassemble = \i' _ _ _ -> mkVar i' idx
       }
   NIdt (Ident i sym) ->
     NodeDetails
@@ -299,7 +293,7 @@ destruct = \case
         _nodeChildren = [],
         _nodeChildBindersNum = [],
         _nodeChildBindersInfo = [],
-        _nodeReassemble = \i' _ _ -> mkIdent i' sym
+        _nodeReassemble = \i' _ _ _ -> mkIdent i' sym
       }
   NCst (Constant i c) ->
     NodeDetails
@@ -308,7 +302,7 @@ destruct = \case
         _nodeChildren = [],
         _nodeChildBindersNum = [],
         _nodeChildBindersInfo = [],
-        _nodeReassemble = \i' _ _ -> mkConstant i' c
+        _nodeReassemble = \i' _ _ _ -> mkConstant i' c
       }
   NApp (App i l r) ->
     NodeDetails
@@ -317,7 +311,7 @@ destruct = \case
         _nodeChildren = [l, r],
         _nodeChildBindersNum = [0, 0],
         _nodeChildBindersInfo = [[], []],
-        _nodeReassemble = \i' _ args' -> mkApp i' (hd args') (args' !! 1)
+        _nodeReassemble = \i' _ _ args' -> mkApp i' (hd args') (args' !! 1)
       }
   NBlt (BuiltinApp i op args) ->
     NodeDetails
@@ -326,7 +320,7 @@ destruct = \case
         _nodeChildren = args,
         _nodeChildBindersNum = map (const 0) args,
         _nodeChildBindersInfo = map (const []) args,
-        _nodeReassemble = \i' _ args' -> mkBuiltinApp i' op args'
+        _nodeReassemble = \i' _ _ args' -> mkBuiltinApp i' op args'
       }
   NCtr (Constr i tag args) ->
     NodeDetails
@@ -335,39 +329,39 @@ destruct = \case
         _nodeChildren = args,
         _nodeChildBindersNum = map (const 0) args,
         _nodeChildBindersInfo = map (const []) args,
-        _nodeReassemble = \i' _ args' -> mkConstr i' tag args'
+        _nodeReassemble = \i' _ _ args' -> mkConstr i' tag args'
       }
-  NLam (Lambda i b) ->
+  NLam (Lambda i bi b) ->
     NodeDetails
       { _nodeInfo = i,
         _nodeSubinfos = [],
         _nodeChildren = [b],
         _nodeChildBindersNum = [1],
-        _nodeChildBindersInfo = [fetchBinderInfo i],
-        _nodeReassemble = \i' _ args' -> mkLambda i' (hd args')
+        _nodeChildBindersInfo = [[bi]],
+        _nodeReassemble = \i' _ binders args' -> mkLambda i' (hd binders) (hd args')
       }
-  NLet (Let i v b) ->
+  NLet (Let i (LetItem bi v) b) ->
     NodeDetails
       { _nodeInfo = i,
         _nodeSubinfos = [],
         _nodeChildren = [v, b],
         _nodeChildBindersNum = [0, 1],
-        _nodeChildBindersInfo = [[], fetchBinderInfo i],
-        _nodeReassemble = \i' _ args' -> mkLet i' (hd args') (args' !! 1)
+        _nodeChildBindersInfo = [[], [bi]],
+        _nodeReassemble = \i' _ binders args' -> mkLet i' (hd binders) (hd args') (args' !! 1)
       }
   NRec (LetRec i vs b) ->
     let n = length vs
      in NodeDetails
           { _nodeInfo = i,
             _nodeSubinfos = [],
-            _nodeChildren = b : toList vs,
+            _nodeChildren = b : map (^. letItemValue) (toList vs),
             _nodeChildBindersNum = replicate (n + 1) n,
-            _nodeChildBindersInfo = replicate (n + 1) (getInfoBinders n i),
-            _nodeReassemble = \i' _ args' -> mkLetRec i' (fromList (tl args')) (hd args')
+            _nodeChildBindersInfo = replicate (n + 1) (map (^. letItemBinder) (toList vs)),
+            _nodeReassemble = \i' _ binders args' -> mkLetRec i' (nonEmpty' (tl (zip binders args'))) (hd args')
           }
   NCase (Case i v bs Nothing) ->
     let branchBinderNums = map (^. caseBranchBindersNum) bs
-        branchBinderInfos = map (\(CaseBranch {..}) -> getInfoBinders _caseBranchBindersNum _caseBranchInfo) bs
+        branchBinderInfos = map (\CaseBranch {..} -> getInfoBinders _caseBranchBindersNum _caseBranchInfo) bs
      in NodeDetails
           { _nodeInfo = i,
             _nodeSubinfos = map (^. caseBranchInfo) bs,
@@ -393,7 +387,7 @@ destruct = \case
           }
   NCase (Case i v bs (Just def)) ->
     let branchBinderNums = map (^. caseBranchBindersNum) bs
-        branchBinderInfos = map (\(CaseBranch {..}) -> getInfoBinders _caseBranchBindersNum _caseBranchInfo) bs
+        branchBinderInfos = map (\CaseBranch {..} -> getInfoBinders _caseBranchBindersNum _caseBranchInfo) bs
      in NodeDetails
           { _nodeInfo = i,
             _nodeSubinfos = map (^. caseBranchInfo) bs,
@@ -445,12 +439,12 @@ destruct = \case
             _nodeReassemble = \i' is' args' ->
               mkMatch
                 i'
-                (fromList $ List.take n args')
+                (nonEmpty' $ take n args')
                 ( zipWithExact
                     ( \br body' ->
                         br
                           { _matchBranchPatterns =
-                              fromList $ setPatternsInfos is' (toList (br ^. matchBranchPatterns)),
+                              nonEmpty' $ setPatternsInfos is' (toList (br ^. matchBranchPatterns)),
                             _matchBranchBody = body'
                           }
                     )
@@ -458,13 +452,13 @@ destruct = \case
                     (drop n args')
                 )
           }
-  NPi (Pi i ty b) ->
+  NPi (Pi i bi b) ->
     NodeDetails
       { _nodeInfo = i,
         _nodeSubinfos = [],
-        _nodeChildren = [ty, b],
+        _nodeChildren = [bi ^. binderType, b],
         _nodeChildBindersNum = [0, 1],
-        _nodeChildBindersInfo = [[], fetchBinderInfo i],
+        _nodeChildBindersInfo = [[], [bi]],
         _nodeReassemble = \i' _ args' -> mkPi i' (hd args') (args' !! 1)
       }
   NUniv (Univ i l) ->
@@ -503,18 +497,19 @@ destruct = \case
         _nodeChildBindersInfo = [],
         _nodeReassemble = \i' _ _ -> mkDynamic i'
       }
-  Closure env (Lambda i b) ->
+  Closure env (Lambda i bi b) ->
     NodeDetails
       { _nodeInfo = i,
         _nodeSubinfos = [],
         _nodeChildren = b : env,
         _nodeChildBindersNum = 1 : map (const 0) env,
-        _nodeChildBindersInfo = fetchBinderInfo i : map (const []) env,
-        _nodeReassemble = \i' _ args' -> Closure (tl args') (Lambda i' (hd args'))
+        _nodeChildBindersInfo = [bi] : map (const []) env,
+        _nodeReassemble = \i' _ args' -> Closure (tl args') (Lambda i' bi (hd args'))
       }
   where
     fetchBinderInfo :: Info -> [Info]
-    fetchBinderInfo i = [getInfoBinder i]
+    -- fetchBinderInfo i = [getInfoBinder i]
+    fetchBinderInfo i = undefined
 
     setPatternsInfos :: [Info] -> [Pattern] -> [Pattern]
     setPatternsInfos is ps = snd $ setPatternsInfos' is ps
diff --git a/src/Juvix/Compiler/Core/Extra/Stripped/Base.hs b/src/Juvix/Compiler/Core/Extra/Stripped/Base.hs
index b79c64d7e0..d60df9252b 100644
--- a/src/Juvix/Compiler/Core/Extra/Stripped/Base.hs
+++ b/src/Juvix/Compiler/Core/Extra/Stripped/Base.hs
@@ -33,7 +33,20 @@ mkConstr' :: Symbol -> Tag -> [Node] -> Node
 mkConstr' sym = mkConstr (ConstrInfo Nothing TyDynamic sym)
 
 mkLet :: LetInfo -> Node -> Node -> Node
-mkLet i v b = NLet (Let i v b)
+mkLet i v b = NLet (Let i item b)
+  where
+    item :: LetItem
+    item =
+      LetItem
+        { _letItemBinder = error "TODO",
+          _letItemValue = v
+        }
+    binder :: Binder' Type
+    binder =
+      Binder
+        { _binderName = i ^. letInfoBinderName,
+          _binderType = i ^. letInfoBinderType
+        }
 
 mkLet' :: Node -> Node -> Node
 mkLet' = mkLet (LetInfo Nothing TyDynamic)
diff --git a/src/Juvix/Compiler/Core/Language.hs b/src/Juvix/Compiler/Core/Language.hs
index 4c090a2c98..a54009bc36 100644
--- a/src/Juvix/Compiler/Core/Language.hs
+++ b/src/Juvix/Compiler/Core/Language.hs
@@ -21,6 +21,10 @@ type BuiltinApp = BuiltinApp' Info Node
 
 type Constr = Constr' Info Node
 
+type Binder = Binder' Node
+
+type LambdaLhs = LambdaLhs' Info Node
+
 type Lambda = Lambda' Info Node
 
 type Let = Let' Info Node
@@ -41,7 +45,7 @@ type PatternBinder = PatternBinder' Info
 
 type PatternConstr = PatternConstr' Info
 
-type Pattern = Pattern' Info
+type Pattern = Pattern' Info Node
 
 type Pi = Pi' Info Node
 
@@ -123,3 +127,10 @@ instance HasAtomicity Node where
     NPrim x -> atomicity x
     NDyn x -> atomicity x
     Closure {} -> Aggregate lambdaFixity
+
+emptyBinder :: Binder
+emptyBinder =
+  Binder
+    { _binderName = Nothing,
+      _binderType = NDyn (Dynamic mempty)
+    }
diff --git a/src/Juvix/Compiler/Core/Language/Nodes.hs b/src/Juvix/Compiler/Core/Language/Nodes.hs
index 8e7a086e13..432a036c3a 100644
--- a/src/Juvix/Compiler/Core/Language/Nodes.hs
+++ b/src/Juvix/Compiler/Core/Language/Nodes.hs
@@ -23,6 +23,13 @@ data ConstantValue
   | ConstString !Text
   deriving stock (Eq)
 
+-- | Info about a single binder. Associated with Lambda and Pi.
+data Binder' a = Binder
+  {
+   _binderName :: Maybe Name,
+   _binderType :: a
+  }
+
 -- Other things we might need in the future:
 -- - ConstFloat or ConstFixedPoint
 
@@ -59,8 +66,15 @@ data Constr' i a = Constr
     _constrArgs :: ![a]
   }
 
+-- | Useful for unfolding lambdas
+data LambdaLhs' i a = LambdaLhs {
+  _lambdaLhsInfo :: i,
+  _lambdaLhsBinder :: Binder' a
+  }
+
 data Lambda' i a = Lambda
   { _lambdaInfo :: i,
+    _lambdaBinder :: Binder' a,
     _lambdaBody :: !a
   }
 
@@ -68,16 +82,21 @@ data Lambda' i a = Lambda
 -- purposes of ML-polymorphic / dependent type checking or code generation!
 data Let' i a = Let
   { _letInfo :: i,
-    _letValue :: !a,
+    _letItem :: {-# UNPACK #-} !(LetItem' a),
     _letBody :: !a
   }
 
+data LetItem' a = LetItem {
+  _letItemBinder :: Binder' a,
+  _letItemValue :: a
+  }
+
 -- | Represents a block of mutually recursive local definitions. Both in the
 -- body and in the values `length _letRecValues` implicit binders are introduced
 -- which hold the functions/values being defined.
 data LetRec' i a = LetRec
   { _letRecInfo :: i,
-    _letRecValues :: !(NonEmpty a),
+    _letRecValues :: !(NonEmpty (LetItem' a)),
     _letRecBody :: !a
   }
 
@@ -115,29 +134,29 @@ data Match' i a = Match
 -- 2)) (Var 1)) (Var 0)'. So the de Bruijn indices increase from right to left.
 data MatchBranch' i a = MatchBranch
   { _matchBranchInfo :: i,
-    _matchBranchPatterns :: !(NonEmpty (Pattern' i)),
+    _matchBranchPatterns :: !(NonEmpty (Pattern' i a)),
     _matchBranchBody :: !a
   }
 
-data Pattern' i
+data Pattern' i a
   = PatWildcard (PatternWildcard' i)
-  | PatBinder (PatternBinder' i)
-  | PatConstr (PatternConstr' i)
-  deriving stock (Eq)
+  | PatBinder (PatternBinder' i a)
+  | PatConstr (PatternConstr' i a)
 
 newtype PatternWildcard' i = PatternWildcard
   { _patternWildcardInfo :: i
   }
 
-data PatternBinder' i = PatternBinder
+data PatternBinder' i a = PatternBinder
   { _patternBinderInfo :: i,
-    _patternBinderPattern :: Pattern' i
+    _patternBinder :: Binder' a,
+    _patternBinderPattern :: Pattern' i a
   }
 
-data PatternConstr' i = PatternConstr
+data PatternConstr' i a = PatternConstr
   { _patternConstrInfo :: i,
     _patternConstrTag :: !Tag,
-    _patternConstrArgs :: ![Pattern' i]
+    _patternConstrArgs :: ![Pattern' i a]
   }
 
 -- | Dependent Pi-type. Compilation-time only. Pi implicitly introduces a binder
@@ -145,10 +164,17 @@ data PatternConstr' i = PatternConstr
 -- body` in more familiar notation, but references to `x` in `body` are via de
 -- Bruijn index. For example, Pi A : Type . A -> A translates to (omitting
 -- Infos): Pi (Univ level) (Pi (Var 0) (Var 1)).
-data Pi' i a = Pi {_piInfo :: i, _piType :: !a, _piBody :: !a}
+data Pi' i a = Pi
+  { _piInfo :: i,
+    _piBinder :: Binder' a,
+    _piBody :: !a
+  }
 
 -- | Universe. Compilation-time only.
-data Univ' i = Univ {_univInfo :: i, _univLevel :: !Int}
+data Univ' i = Univ
+  { _univInfo :: i,
+    _univLevel :: !Int
+  }
 
 -- | Type constructor application. Compilation-time only.
 data TypeConstr' i a = TypeConstr
@@ -214,15 +240,15 @@ instance HasAtomicity (Match' i a) where
 instance HasAtomicity (PatternWildcard' i) where
   atomicity _ = Atom
 
-instance HasAtomicity (PatternBinder' i) where
+instance HasAtomicity (PatternBinder' i a) where
   atomicity _ = Atom
 
-instance HasAtomicity (PatternConstr' i) where
+instance HasAtomicity (PatternConstr' i a) where
   atomicity PatternConstr {..}
     | null _patternConstrArgs = Atom
     | otherwise = Aggregate appFixity
 
-instance HasAtomicity (Pattern' i) where
+instance HasAtomicity (Pattern' i a) where
   atomicity = \case
     PatWildcard x -> atomicity x
     PatBinder x -> atomicity x
@@ -246,6 +272,29 @@ instance HasAtomicity (Dynamic' i) where
 lambdaFixity :: Fixity
 lambdaFixity = Fixity (PrecNat 0) (Unary AssocPostfix)
 
+makeLenses ''Binder'
+makeLenses ''Var'
+makeLenses ''Ident'
+makeLenses ''Constant'
+makeLenses ''App'
+makeLenses ''BuiltinApp'
+makeLenses ''Constr'
+makeLenses ''Let'
+makeLenses ''LetRec'
+makeLenses ''Case'
+makeLenses ''CaseBranch'
+makeLenses ''Match'
+makeLenses ''MatchBranch'
+makeLenses ''PatternWildcard'
+makeLenses ''PatternBinder'
+makeLenses ''PatternConstr'
+makeLenses ''Pi'
+makeLenses ''Lambda'
+makeLenses ''Univ'
+makeLenses ''TypeConstr'
+makeLenses ''Dynamic'
+makeLenses ''LetItem'
+
 instance Eq (Var' i) where
   (Var _ idx1) == (Var _ idx2) = idx1 == idx2
 
@@ -267,15 +316,6 @@ instance Eq a => Eq (BuiltinApp' i a) where
 instance Eq a => Eq (Constr' i a) where
   (Constr _ tag1 args1) == (Constr _ tag2 args2) = tag1 == tag2 && args1 == args2
 
-instance Eq a => Eq (Lambda' i a) where
-  (Lambda _ b1) == (Lambda _ b2) = b1 == b2
-
-instance Eq a => Eq (Let' i a) where
-  (Let _ v1 b1) == (Let _ v2 b2) = v1 == v2 && b1 == b2
-
-instance Eq a => Eq (LetRec' i a) where
-  (LetRec _ vs1 b1) == (LetRec _ vs2 b2) = vs1 == vs2 && b1 == b2
-
 instance Eq a => Eq (Case' i bi a) where
   (Case _ v1 bs1 def1) == (Case _ v2 bs2 def2) = v1 == v2 && bs1 == bs2 && def1 == def2
 
@@ -285,21 +325,9 @@ instance Eq a => Eq (CaseBranch' i a) where
 instance Eq a => Eq (Match' i a) where
   (Match _ vs1 bs1) == (Match _ vs2 bs2) = vs1 == vs2 && bs1 == bs2
 
-instance Eq a => Eq (MatchBranch' i a) where
-  (MatchBranch _ pats1 b1) == (MatchBranch _ pats2 b2) = pats1 == pats2 && b1 == b2
-
 instance Eq (PatternWildcard' i) where
   _ == _ = True
 
-instance Eq (PatternBinder' i) where
-  (PatternBinder _ p1) == (PatternBinder _ p2) = p1 == p2
-
-instance Eq (PatternConstr' i) where
-  (PatternConstr _ tag1 ps1) == (PatternConstr _ tag2 ps2) = tag1 == tag2 && ps1 == ps2
-
-instance Eq a => Eq (Pi' i a) where
-  (Pi _ ty1 b1) == (Pi _ ty2 b2) = ty1 == ty2 && b1 == b2
-
 instance Eq (Univ' i) where
   (Univ _ l1) == (Univ _ l2) = l1 == l2
 
@@ -312,26 +340,37 @@ instance Eq (TypePrim' i) where
 instance Eq (Dynamic' i) where
   (Dynamic _) == (Dynamic _) = True
 
-makeLenses ''Var'
-makeLenses ''Ident'
-makeLenses ''Constant'
-makeLenses ''App'
-makeLenses ''BuiltinApp'
-makeLenses ''Constr'
-makeLenses ''Let'
-makeLenses ''LetRec'
-makeLenses ''Case'
-makeLenses ''CaseBranch'
-makeLenses ''Match'
-makeLenses ''MatchBranch'
-makeLenses ''PatternWildcard'
-makeLenses ''PatternBinder'
-makeLenses ''PatternConstr'
-makeLenses ''Pi'
-makeLenses ''Lambda'
-makeLenses ''Univ'
-makeLenses ''TypeConstr'
-makeLenses ''Dynamic'
+deriving stock instance Eq a => Eq (Pattern' i a)
+
+instance Eq a => Eq (LetItem' a) where
+  (==) = eqOn (^. letItemValue)
+
+-- | ignores the binder
+instance Eq a => Eq (Lambda' i a) where
+  (==) = eqOn (^. lambdaBody)
+
+-- | ignores the binder
+instance Eq a => Eq (Let' i a) where
+  (==) = eqOn (^. letItem)
+    ..&&.. eqOn (^. letBody)
+
+instance Eq a => Eq (LetRec' i a) where
+  (==) = eqOn (^. letRecBody)
+    ..&&.. eqOn (^. letRecValues)
+
+instance Eq a => Eq (Pi' i a) where
+  (==) = eqOn (^. piBinder . binderType)
+   ..&&.. eqOn (^. piBody)
+
+-- | ignores the binder
+instance Eq a => Eq (PatternBinder' i a) where
+  (==) = eqOn (^. patternBinderPattern)
+
+instance Eq a => Eq (MatchBranch' i a) where
+  (MatchBranch _ pats1 b1) == (MatchBranch _ pats2 b2) = pats1 == pats2 && b1 == b2
+
+instance Eq a => Eq (PatternConstr' i a) where
+  (PatternConstr _ tag1 ps1) == (PatternConstr _ tag2 ps2) = tag1 == tag2 && ps1 == ps2
 
 instance Hashable (Ident' i) where
   hashWithSalt s = hashWithSalt s . (^. identSymbol)
diff --git a/src/Juvix/Compiler/Core/Language/Stripped.hs b/src/Juvix/Compiler/Core/Language/Stripped.hs
index ce4c68c528..c014a52a90 100644
--- a/src/Juvix/Compiler/Core/Language/Stripped.hs
+++ b/src/Juvix/Compiler/Core/Language/Stripped.hs
@@ -56,13 +56,17 @@ type Constant = Constant' ()
 
 type Apps = Apps' Fun () Node
 
-data Fun = FunVar Var | FunIdent Ident
+data Fun =
+  FunVar Var
+  | FunIdent Ident
   deriving stock (Eq)
 
 type BuiltinApp = BuiltinApp' () Node
 
 type Constr = Constr' ConstrInfo Node
 
+type LetItem = LetItem' Node
+
 type Let = Let' LetInfo Node
 
 type Case = Case' CaseInfo CaseBranchInfo Node
diff --git a/src/Juvix/Compiler/Core/Language/Stripped/Type.hs b/src/Juvix/Compiler/Core/Language/Stripped/Type.hs
index 76cfde854c..ddef4c7e28 100644
--- a/src/Juvix/Compiler/Core/Language/Stripped/Type.hs
+++ b/src/Juvix/Compiler/Core/Language/Stripped/Type.hs
@@ -3,7 +3,11 @@ module Juvix.Compiler.Core.Language.Stripped.Type where
 import Juvix.Compiler.Core.Language.Base
 import Juvix.Compiler.Core.Language.Primitives
 
-data Type = TyDynamic | TyPrim Primitive | TyApp TypeApp | TyFun TypeFun
+data Type
+  = TyDynamic
+  | TyPrim Primitive
+  | TyApp TypeApp
+  | TyFun TypeFun
   deriving stock (Eq)
 
 data TypeApp = TypeApp
diff --git a/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs b/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs
index 37142dc426..f9326760b3 100644
--- a/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs
+++ b/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs
@@ -11,3 +11,6 @@ fromMain = error "not yet implemented"
 
 translateNode :: Node -> Stripped.Node
 translateNode _ = Stripped.mkVar' 0
+
+translateType :: Node -> Stripped.Type
+translateType _ = error "not yet implemented"
diff --git a/src/Juvix/Prelude/Base.hs b/src/Juvix/Prelude/Base.hs
index bfc9234a8a..a08f023490 100644
--- a/src/Juvix/Prelude/Base.hs
+++ b/src/Juvix/Prelude/Base.hs
@@ -256,6 +256,9 @@ commonPrefix a b = reverse (go [] a b)
 -- NonEmpty
 --------------------------------------------------------------------------------
 
+nonEmpty' :: [a] -> NonEmpty a
+nonEmpty' = NonEmpty.fromList
+
 nonEmptyUnsnoc :: NonEmpty a -> (Maybe (NonEmpty a), a)
 nonEmptyUnsnoc e = (NonEmpty.nonEmpty (NonEmpty.init e), NonEmpty.last e)
 
@@ -363,13 +366,21 @@ readerState m = get >>= (`runReader` m)
 infixr 3 .&&.
 
 (.&&.) :: (a -> Bool) -> (a -> Bool) -> a -> Bool
-(a .&&. b) c = a c && b c
+(f .&&. g) a = f a && g a
+
+infixr 3 ..&&..
+
+(..&&..) :: (a -> b -> Bool) -> (a -> b -> Bool) -> (a -> b -> Bool)
+(f ..&&.. g) a = f a .&&. g a
 
 infixr 2 .||.
 
 (.||.) :: (a -> Bool) -> (a -> Bool) -> a -> Bool
 (a .||. b) c = a c || b c
 
+eqOn :: Eq b => (a -> b) -> a -> a -> Bool
+eqOn = ((==) `on`)
+
 class CanonicalProjection a b where
   project :: a -> b