diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -2,6 +2,13 @@
 
 ## version 0
 
+### 0.2 -- 2023-10-06
+
+* Add operations for list.
+* Integrate mkFree function into Var and Binder.
+* Now MkFree requires monadic instance.
+* Binder requires Monad typeclass.
+
 ### 0.1 -- 2023-10-04
 
 Initial release.
diff --git a/binder.cabal b/binder.cabal
--- a/binder.cabal
+++ b/binder.cabal
@@ -1,6 +1,6 @@
 cabal-version:      3.0
 name:               binder
-version:            0.1
+version:            0.2
 synopsis:           Variable binding for abstract syntax tree
 description:
     binder is purely functional implementation of Ocaml's
@@ -29,11 +29,12 @@
 source-repository this
     type:     git
     location: https://github.com/ijaketak/binder
-    tag:      0.1
+    tag:      0.2
 
 common depends
     build-depends:
           containers < 0.8
+        , lens < 5.3
         , text < 2.2
         , transformers < 0.7
 
@@ -48,7 +49,6 @@
     -- other-extensions:
     build-depends:
           base < 4.19
-        , lens < 5.3
     hs-source-dirs:   src
     default-language: Haskell2010
 
@@ -58,6 +58,7 @@
     other-modules:
           Binder1Spec
         , Binder2Spec
+        , Binder3Spec
     -- other-extensions:
     type:             exitcode-stdio-1.0
     hs-source-dirs:   test
diff --git a/src/Data/Binder.hs b/src/Data/Binder.hs
--- a/src/Data/Binder.hs
+++ b/src/Data/Binder.hs
@@ -24,10 +24,10 @@
 -- * Variable and Box
   , Var
   , Box
-  , MkFree(..)
 -- ** Variable
   , var'Key
   , var'Name
+  , var'mkFree
   , var'Box
   , nameOf
   , boxVar
@@ -45,9 +45,12 @@
   , boxPair
   , boxTriple
   , boxT
+  , boxList
+  , boxJoin
 -- * Variable binding
   , Binder
   , binder'Name
+  , binder'mkFree
   , binder'Body
   , subst
   , buildBinder
@@ -55,9 +58,32 @@
   , unbind
   , eqBinder
   , boxBinder
+  , bindApply
+-- * List
+-- * Variable list
+  , VarList
+  , varList'Keys
+  , varList'Names
+  , varList'Boxes
+  , namesOf
+  , boxVarList
+  , newVarList
+-- * Binder for list
+  , BinderList
+  , binderList'Names
+  , binderList'Body
+  , binderList'mkFree
+  , binderList'Arity
+  , substList
+  , eqBinderList
+  , bindList
+  , unbindList
+  , boxBinderList
+  , bindListApply
   ) where
 
 import Control.Lens
+import Control.Monad (join)
 import Data.Kind (Type)
 import qualified Data.Map.Lazy as M
 import Data.Maybe (fromJust)
@@ -78,6 +104,7 @@
   }
 data VarBody m a = VarBody
   { _varBody'Name :: Text
+  , _varBody'mkFree :: Var m a -> m a
   , _varBody'Box :: Box m a
   }
 -- | Representation of under-construction things
@@ -86,23 +113,22 @@
   = Box'Closed a
   | Box'Env (EnvVar m) (Closure m a)
 
--- | Typeclass for free variable constructor.
-class MkFree m a where
-  mkFree :: Var m a -> a
-
-data AnyVar m = forall a. MkFree m a => AnyVar (Var m a)
+data AnyVar m = forall a. AnyVar (Var m a)
 type EnvVar m = M.Map (Numbering m) (AnyVar m)
-data AnyMkFree m = forall a. MkFree m a => AnyMkFree a
-type EnvMkFree m = M.Map (Numbering m) (AnyMkFree m)
-newtype Closure m a = Closure { unClosure :: (EnvMkFree m) -> a }
+data AnyOne = forall a. AnyOne a
+type EnvOne m = M.Map (Numbering m) AnyOne
+newtype Closure m a = Closure { unClosure :: (EnvOne m) -> m a }
 
-instance Functor (Closure m) where
-  fmap f cla = Closure $ f . unClosure cla
+instance Functor m => Functor (Closure m) where
+  fmap f cla = Closure $ fmap f . unClosure cla
 
-instance Applicative (Closure m) where
-  pure a = Closure $ const a
-  clf <*> cla = Closure $ \env -> unClosure clf env $ unClosure cla env
+instance Applicative m => Applicative (Closure m) where
+  pure a = Closure $ const $ pure a
+  clf <*> cla = Closure $ \env -> unClosure clf env <*> unClosure cla env
 
+closureJoin :: Monad m => Closure m (m a) -> Closure m a
+closureJoin cl = Closure $ \env -> join $ unClosure cl env
+
 instance MonadNumbering m => Eq (Var m a) where
   Var x _ == Var y _ = x == y
 
@@ -115,6 +141,8 @@
 
 var'Name :: Lens' (Var m a) Text
 var'Name = var'Body . varBody'Name
+var'mkFree :: Lens' (Var m a) (Var m a -> m a)
+var'mkFree = var'Body . varBody'mkFree
 var'Box :: Lens' (Var m a) (Box m a)
 var'Box = var'Body . varBody'Box
 
@@ -134,15 +162,15 @@
 boxVar x = x ^. var'Box
 
 -- | Create a new variable with given name.
-newVar :: forall m a. (MkFree m a, MonadNumbering m) => Text -> m (Var m a)
-newVar name = do
+newVar :: forall m a. MonadNumbering m => Text -> (Var m a -> m a) -> m (Var m a)
+newVar name mkFree = do
   i <- numbering
   let x = let b = Box'Env
                 (M.singleton i $ AnyVar x)
                 (Closure $ \env ->
-                  let f (AnyMkFree y) = unsafeCoerce y
+                  let f (AnyOne y) = pure $ unsafeCoerce y
                    in f $ fromJust $ M.lookup i env)
-           in Var i $ VarBody name b
+           in Var i $ VarBody name mkFree b
   return x
 
 
@@ -157,31 +185,31 @@
 occur v (Box'Env vs _) = M.member (v ^. var'Key) vs
 
 
-instance Functor (Box m) where
+instance Functor m => Functor (Box m) where
   fmap f (Box'Closed a) = Box'Closed (f a)
   fmap f (Box'Env vs ta) = Box'Env vs (f <$> ta)
 
-instance (MonadNumbering m) => Applicative (Box m) where
+instance MonadNumbering m => Applicative (Box m) where
   pure = Box'Closed
   Box'Closed f <*> Box'Closed a = Box'Closed (f a)
   Box'Closed f <*> Box'Env va ta = Box'Env va (f <$> ta)
   Box'Env vf tf <*> Box'Closed a = Box'Env vf (appClosure tf a)
    where
-    appClosure clf x = Closure $ \env -> unClosure clf env x
+    appClosure clf x = Closure $ \env -> unClosure clf env <*> pure x
   Box'Env vf tf <*> Box'Env va ta = Box'Env (M.union vf va) (tf <*> ta)
 
 -- | Pick out and complete the construction of @a@.
-unbox :: forall m a. Box m a -> a
-unbox (Box'Closed t) = t
-unbox (Box'Env env cl) = unClosure cl $ f <$> env
+unbox :: forall m a. Monad m => Box m a -> m a
+unbox (Box'Closed t) = pure t
+unbox (Box'Env env cl) = unClosure cl =<< traverse f env
  where
-  f (AnyVar x) = AnyMkFree @m $ mkFree x
+  f (AnyVar x) = fmap AnyOne $ x ^. var'mkFree $ x
 
 box :: MonadNumbering m => a -> Box m a
 box = pure
 apBox :: MonadNumbering m => Box m (a -> b) -> Box m a -> Box m b
 apBox = (<*>)
-boxApply :: (a -> b) -> Box m a -> Box m b
+boxApply :: Functor m => (a -> b) -> Box m a -> Box m b
 boxApply = fmap
 boxApply2 :: MonadNumbering m => (a -> b -> c) -> Box m a -> Box m b -> Box m c
 boxApply2 f ta tb = f <$> ta <*> tb
@@ -195,61 +223,183 @@
 boxTriple = boxApply3 (,,)
 boxT :: (MonadNumbering m, Traversable t) => t (Box m a) -> Box m (t a)
 boxT = sequenceA
+boxList :: MonadNumbering m => [Box m a] -> Box m [a]
+boxList = sequenceA
+boxJoin :: MonadNumbering m => Box m (m a) -> m (Box m a)
+boxJoin (Box'Closed ma) = return . Box'Closed =<< ma
+boxJoin (Box'Env env cl) = return $ Box'Env env $ closureJoin cl
 
 
 -- | Variable binding.
---   Essentially, @Binder a b@ means @a -> b@.
-data Binder a b = Binder
+--   Essentially, @Binder a m b@ means @a -> m b@.
+data Binder a m b = Binder
   { _binder'Name :: Text
-  , _binder'Body :: a -> b
+  , _binder'mkFree :: Var m a -> m a
+  , _binder'Body :: a -> m b
   }
 
 $(makeLenses ''Binder)
 
 -- | Variable substitution.
-subst :: Binder a b -> a -> b
+subst :: Binder a m b -> a -> m b
 subst b = b ^. binder'Body
 
 -- | unbinding
-unbind :: (MkFree m a, MonadNumbering m) => Binder a b -> m (Var m a, b)
+unbind :: MonadNumbering m => Binder a m b -> m (Var m a, b)
 unbind b = do
-  x <- newVar $ b ^. binder'Name
-  return (x, subst b $ mkFree x)
+  let mkFree = b ^. binder'mkFree
+  x <- newVar (b ^. binder'Name) mkFree
+  y <- subst b =<< mkFree x
+  return (x, y)
 
-unbind2 :: (MkFree m a, MonadNumbering m)
-        => Binder a b1 -> Binder a b2 -> m (Var m a, b1, b2)
+unbind2 :: MonadNumbering m
+        => Binder a m b1 -> Binder a m b2 -> m (Var m a, b1, b2)
 unbind2 b1 b2 = do
-  x <- newVar $ b1 ^. binder'Name
-  let v = mkFree x
-  return (x, subst b1 v, subst b2 v)
+  let mkFree = b1 ^. binder'mkFree
+  x <- newVar (b1 ^. binder'Name) mkFree
+  v <- mkFree x
+  y1 <- subst b1 v
+  y2 <- subst b2 v
+  return (x, y1, y2)
 
 -- | Check if two bindings are equal.
-eqBinder :: (MkFree m a, MonadNumbering m)
-         => (b -> b -> m Bool) -> Binder a b -> Binder a b -> m Bool
+eqBinder :: MonadNumbering m
+         => (b -> b -> m Bool) -> Binder a m b -> Binder a m b -> m Bool
 eqBinder eq f g = do
   (_, t, u) <- unbind2 f g
   eq t u
 
 
 -- | Smart constructor for 'Binder'.
-buildBinder :: Var m a -> (a -> b) -> Binder a b
-buildBinder x body = Binder (x ^. var'Name) body
+buildBinder :: Var m a -> (a -> m b) -> Binder a m b
+buildBinder x body = Binder (x ^. var'Name) (x ^. var'mkFree) body
 
 -- | binding
-bind :: (MkFree m a, MonadNumbering m)
-        => Var m a -> Box m b -> Box m (Binder a b)
-bind x (Box'Closed t) = Box'Closed $ buildBinder x $ const t
+bind :: MonadNumbering m => Var m a -> Box m b -> Box m (Binder a m b)
+bind x (Box'Closed t) = Box'Closed $ buildBinder x $ const $ return t
 bind x (Box'Env vs t) =
   let vs' = M.delete (x ^. var'Key) vs in if length vs' == 0
     then Box'Closed $ buildBinder x $
-      \arg -> unClosure t $ M.singleton (x ^. var'Key) (AnyMkFree arg)
+      \arg -> unClosure t $ M.singleton (x ^. var'Key) (AnyOne arg)
     else Box'Env vs' $ Closure $
-      \ms -> buildBinder x $
-      \arg -> unClosure t $ M.insert (x ^. var'Key) (AnyMkFree arg) ms
+      \ms -> return $ buildBinder x $
+      \arg -> unClosure t $ M.insert (x ^. var'Key) (AnyOne arg) ms
 
-boxBinder :: (MkFree m a, MonadNumbering m)
-          => (b -> m (Box m b)) -> Binder a b -> m (Box m (Binder a b))
+boxBinder :: MonadNumbering m
+          => (b -> m (Box m b)) -> Binder a m b -> m (Box m (Binder a m b))
 boxBinder f b = do
   (x, t) <- unbind b
   ft <- f t
   return $ bind x ft
+
+bindApply :: MonadNumbering m => Box m (Binder a m b) -> Box m a -> m (Box m b)
+bindApply b arg = boxJoin $ subst <$> b <*> arg
+
+
+type VarList m a = [Var m a]
+
+varList'Keys :: Getter (VarList m a) [Numbering m]
+varList'Keys = to $ fmap $ view var'Key
+varList'Names :: Getter (VarList m a) [Text]
+varList'Names = to $ fmap $ view var'Name
+varList'Boxes :: Getter (VarList m a) [Box m a]
+varList'Boxes = to $ fmap $ view var'Box
+
+-- | The names of variables.
+namesOf :: VarList m a -> [Text]
+namesOf = fmap $ view var'Name
+
+-- | Smart constructor for a list of 'Box'.
+boxVarList :: VarList m a -> [Box m a]
+boxVarList = fmap $ view var'Box
+
+-- | Create new variables with given names.
+newVarList :: MonadNumbering m => [Text] -> (Var m a -> m a) -> m (VarList m a)
+newVarList names mkFree = sequence $ flip fmap names $ \name -> newVar name mkFree
+
+
+-- | Essentially, @BinderList a m b@ means @[a] -> m b@.
+data BinderList a m b = BinderList
+  { _binderList'Names :: [Text]
+  , _binderList'mkFree :: Var m a -> m a
+  , _binderList'Body :: [a] -> m b
+  }
+
+$(makeLenses ''BinderList)
+
+binderList'Arity :: Getter (BinderList a m b) Int
+binderList'Arity = binderList'Names . to length
+
+-- | Variable substitution.
+substList :: BinderList a m b -> [a] -> m b
+substList ba = ba ^. binderList'Body
+
+-- | unbinding
+unbindList :: MonadNumbering m => BinderList a m b -> m (VarList m a, b)
+unbindList ba = do
+  let mkFree = ba ^. binderList'mkFree
+  xs <- newVarList (ba ^. binderList'Names) mkFree
+  y <- substList ba =<< traverse mkFree xs
+  return (xs, y)
+
+unbind2List :: MonadNumbering m
+             => BinderList a m b1 -> BinderList a m b2
+             -> m (VarList m a, b1, b2)
+unbind2List ba1 ba2 = do
+  let mkFree = ba1 ^. binderList'mkFree
+  xs <- newVarList (ba1 ^. binderList'Names) mkFree
+  vs <- traverse mkFree xs
+  y1 <- substList ba1 vs
+  y2 <- substList ba2 vs
+  return (xs, y1, y2)
+
+-- | Check if two bindings are equal.
+eqBinderList :: MonadNumbering m
+              => (b -> b -> m Bool)
+              -> BinderList a m b -> BinderList a m b -> m Bool
+eqBinderList eq f g =
+  if f ^. binderList'Arity /= g ^. binderList'Arity
+    then return False
+    else do
+      (_, t, u) <- unbind2List f g
+      eq t u
+
+-- | Smart constructor for 'BinderList.
+buildBinderList :: VarList m a -> ([a] -> m b) -> BinderList a m b
+buildBinderList xs body =
+  BinderList (xs ^. varList'Names) (head xs ^. var'mkFree) body
+
+deleteList :: Ord k => [k] -> M.Map k a -> M.Map k a
+deleteList = flip $ foldl $ \m k -> M.delete k m
+insertList :: Ord k => [k] -> [a] -> M.Map k a -> M.Map k a
+insertList ks xs m = foldl f m $ zip ks xs
+ where
+  f n (k, x) = M.insert k x n
+zipList :: Ord k => [k] -> [a] -> M.Map k a
+zipList ks xs = insertList ks xs M.empty
+
+-- | binding
+bindList :: MonadNumbering m
+          => VarList m a -> Box m b -> Box m (BinderList a m b)
+bindList xs (Box'Closed t) = Box'Closed $ buildBinderList xs $ const $ return t
+bindList xs (Box'Env vs t) =
+  let vs' = deleteList (xs ^. varList'Keys) vs in if length vs' == 0
+    then Box'Closed $ buildBinderList xs $
+      \args -> unClosure t $
+      zipList (xs ^. varList'Keys) (AnyOne <$> args)
+    else Box'Env vs' $ Closure $
+      \ms -> return $ buildBinderList xs $
+      \args -> unClosure t $
+      insertList (xs ^. varList'Keys) (AnyOne <$> args) ms
+
+boxBinderList :: MonadNumbering m
+               => (b -> m (Box m b)) -> BinderList a m b
+               -> m (Box m (BinderList a m b))
+boxBinderList f b = do
+  (xs, t) <- unbindList b
+  ft <- f t
+  return $ bindList xs ft
+
+bindListApply :: MonadNumbering m
+              => Box m (BinderList a m b) -> Box m [a] -> m (Box m b)
+bindListApply b args = boxJoin $ substList <$> b <*> args
diff --git a/test/Binder1Spec.hs b/test/Binder1Spec.hs
--- a/test/Binder1Spec.hs
+++ b/test/Binder1Spec.hs
@@ -37,15 +37,15 @@
 
 data Term
   = Term'Var (Var S Term)
-  | Term'Abs (Binder Term Term)
+  | Term'Abs (Binder Term S Term)
   | Term'App Term Term
 
-instance MkFree S Term where
-  mkFree = Term'Var
+term'mkFree :: Var S Term -> S Term
+term'mkFree = return . Term'Var
 
 var :: Var S Term -> Box S Term
 var = boxVar
-absRaw :: Box S (Binder Term Term) -> Box S Term
+absRaw :: Box S (Binder Term S Term) -> Box S Term
 absRaw = fmap Term'Abs
 abs :: Var S Term -> Box S Term -> Box S Term
 abs x t = absRaw $ bind x t
@@ -56,11 +56,13 @@
 boxTerm (Term'Abs b) = absRaw <$> boxBinder boxTerm b
 boxTerm (Term'App t u) = app <$> boxTerm t <*> boxTerm u
 
-eval :: Term -> Term
-eval t@(Term'App f a) = case eval f of
-  Term'Abs b -> eval (subst b a)
-  _ -> t
-eval t = t
+eval :: Term -> S Term
+eval t@(Term'App f a) = do
+  ef <- eval f
+  case ef of
+    Term'Abs b -> eval =<< subst b a
+    _ -> return t
+eval t = return t
 
 size :: Term -> S Int
 size (Term'Var _) = return 0
@@ -86,18 +88,18 @@
 
 termIdentity, termFst, termDelta, termOmega :: S Term
 termIdentity = do
-  x <- newVar "x"
-  return $ unbox $ abs x $ var x
+  x <- newVar "x" term'mkFree
+  unbox $ abs x $ var x
 termFst = do
-  x <- newVar "x"
-  y <- newVar "y"
-  return $ unbox $ abs x $ abs y $ var x
+  x <- newVar "x" term'mkFree
+  y <- newVar "y" term'mkFree
+  unbox $ abs x $ abs y $ var x
 termDelta = do
-  x <- newVar "x"
-  return $ unbox $ abs x $ app (var x) (var x)
+  x <- newVar "x" term'mkFree
+  unbox $ abs x $ app (var x) (var x)
 termOmega = do
   delta <- box <$> termDelta
-  return $ unbox $ app delta delta
+  unbox $ app delta delta
 
 spec :: Spec
 spec = do
diff --git a/test/Binder2Spec.hs b/test/Binder2Spec.hs
--- a/test/Binder2Spec.hs
+++ b/test/Binder2Spec.hs
@@ -39,38 +39,38 @@
 data Ty
   = Ty'Var (Var S Ty)
   | Ty'Arr Ty Ty
-  | Ty'All (Binder Ty Ty)
+  | Ty'All (Binder Ty S Ty)
 
 data Te
   = Te'Var (Var S Te)
-  | Te'Abs Ty (Binder Te Te)
+  | Te'Abs Ty (Binder Te S Te)
   | Te'App Te Te
-  | Te'Lam (Binder Ty Te)
+  | Te'Lam (Binder Ty S Te)
   | Te'Spe Te Ty
 
-instance MkFree S Ty where
-  mkFree = Ty'Var
-instance MkFree S Te where
-  mkFree = Te'Var
+ty'mkFree :: Var S Ty -> S Ty
+ty'mkFree = return . Ty'Var
+te'mkFree :: Var S Te -> S Te
+te'mkFree = return . Te'Var
 
 ty'Var :: Var S Ty -> Box S Ty
 ty'Var = boxVar
 ty'Arr :: Box S Ty -> Box S Ty -> Box S Ty
 ty'Arr a b = Ty'Arr <$> a <*> b
-ty'AllRaw :: Box S (Binder Ty Ty) -> Box S Ty
+ty'AllRaw :: Box S (Binder Ty S Ty) -> Box S Ty
 ty'AllRaw = fmap Ty'All
 ty'All :: Var S Ty -> Box S Ty -> Box S Ty
 ty'All x t = ty'AllRaw $ bind x t
 
 te'Var :: Var S Te -> Box S Te
 te'Var = boxVar
-te'AbsRaw :: Box S Ty -> Box S (Binder Te Te) -> Box S Te
+te'AbsRaw :: Box S Ty -> Box S (Binder Te S Te) -> Box S Te
 te'AbsRaw a f = Te'Abs <$> a <*> f
 te'Abs :: Box S Ty -> Var S Te -> Box S Te -> Box S Te
 te'Abs a x t = te'AbsRaw a $ bind x t
 te'App :: Box S Te -> Box S Te -> Box S Te
 te'App t u = Te'App <$> t <*> u
-te'LamRaw :: Box S (Binder Ty Te) -> Box S Te
+te'LamRaw :: Box S (Binder Ty S Te) -> Box S Te
 te'LamRaw = fmap Te'Lam
 te'Lam :: Var S Ty -> Box S Te -> Box S Te
 te'Lam x t = te'LamRaw $ bind x t
@@ -88,36 +88,41 @@
 boxTe (Te'Lam f) = te'LamRaw <$> boxBinder boxTe f
 boxTe (Te'Spe t a) = te'Spe <$> boxTe t <*> boxTy a
 
-hnf :: Te -> Te
-hnf (Te'App t u) = let v = hnf u in case hnf t of
-  Te'Abs _ b -> hnf $ subst b v
-  h -> Te'App h v
-hnf (Te'Spe t a) = case hnf t of
-  Te'Lam b -> hnf $ subst b a
-  h -> Te'Spe h a
-hnf t = t
+hnf :: Te -> S Te
+hnf (Te'App t u) = do
+  hu <- hnf u
+  ht <- hnf t
+  case ht of
+    Te'Abs _ b -> hnf =<< subst b hu
+    _ -> return $ Te'App ht hu
+hnf (Te'Spe t a) = do
+  ht <- hnf t
+  case ht of
+    Te'Lam b -> hnf =<< subst b a
+    _ -> return $ Te'Spe ht a
+hnf t = return t
 
 nf :: Te -> S Te
 nf (Te'Abs a f) = do
   (x, t) <- unbind f
   nt <- nf t
   bt <- boxTe nt
-  return $ Te'Abs a $ unbox $ bind x bt
+  fmap (Te'Abs a) $ unbox $ bind x bt
 nf (Te'App t u) = do
   nt <- nf t
   nu <- nf u
   case nt of
-    Te'Abs _ f -> nf $ subst f u
+    Te'Abs _ f -> nf =<< subst f u
     _ -> return $ Te'App nt nu
 nf (Te'Lam f) = do
   (x, t) <- unbind f
   nt <- nf t
   bt <- boxTe nt
-  return $ Te'Lam $ unbox $ bind x bt
+  fmap Te'Lam $ unbox $ bind x bt
 nf (Te'Spe t a) = do
   nt <- nf t
   case nt of
-    Te'Lam f -> nf $ subst f a
+    Te'Lam f -> nf =<< subst f a
     _ -> return $ Te'Spe nt a
 nf t = return t
 
@@ -155,12 +160,12 @@
   case mtyt of
     Just tyt -> do
       bt <- boxTy tyt
-      return $ Just $ Ty'All $ unbox $ bind x bt
+      fmap (Just . Ty'All) $ unbox $ bind x bt
     Nothing -> return Nothing
 infer ctxt (Te'Spe t a) = do
   mtyt <- infer ctxt t
   case mtyt of
-    Just (Ty'All f) -> return $ Just $ subst f a
+    Just (Ty'All f) -> Just <$> subst f a
     _ -> return Nothing
 
 check :: Ctxt -> Te -> Ty -> S Bool
@@ -204,21 +209,21 @@
 type1, type2 :: S Ty
 term1 :: S Te
 type1 = do
-  x <- newVar "X"
-  y <- newVar "Y"
-  return $ unbox $ ty'Arr (ty'Var x) (ty'Var y)
+  x <- newVar "X" ty'mkFree
+  y <- newVar "Y" ty'mkFree
+  unbox $ ty'Arr (ty'Var x) (ty'Var y)
 type2 = do
-  x <- newVar "X"
-  y <- newVar "Y"
+  x <- newVar "X" ty'mkFree
+  y <- newVar "Y" ty'mkFree
   let arr = ty'Arr (ty'Var x) (ty'Var y)
-  return $ unbox $ ty'All x $ ty'All y $ ty'Arr arr arr
+  unbox $ ty'All x $ ty'All y $ ty'Arr arr arr
 term1 = do
-  x <- newVar "X"
-  y <- newVar "Y"
-  f <- newVar "f"
-  a <- newVar "a"
+  x <- newVar "X" ty'mkFree
+  y <- newVar "Y" ty'mkFree
+  f <- newVar "f" te'mkFree
+  a <- newVar "a" te'mkFree
   let arr = ty'Arr (ty'Var x) (ty'Var y)
-  return $ unbox $ te'Lam x $ te'Lam y $ te'Abs arr f $ te'Abs (ty'Var x) a $
+  unbox $ te'Lam x $ te'Lam y $ te'Abs arr f $ te'Abs (ty'Var x) a $
     te'App (te'Var f) (te'Var a)
 
 spec :: Spec
diff --git a/test/Binder3Spec.hs b/test/Binder3Spec.hs
new file mode 100644
--- /dev/null
+++ b/test/Binder3Spec.hs
@@ -0,0 +1,334 @@
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module Binder3Spec where
+
+import Control.Lens
+import Control.Monad ((<=<))
+import Control.Monad.IO.Class (MonadIO)
+import Control.Monad.Trans.State.Strict (evalStateT, get, modify, StateT)
+import Data.List (intersperse)
+-- import qualified Data.Map.Lazy as M
+import Data.Text (Text)
+import qualified Data.Text as T (pack)
+import GHC.Generics hiding (S, to)
+import Test.Hspec
+
+import Data.Binder
+
+newtype S a = S { runS :: StateT Int IO a }
+  deriving
+  ( Generic
+  , Generic1
+  , Functor
+  , Applicative
+  , Monad
+  , MonadIO
+  )
+
+instance MonadNumbering S where
+  type Numbering S = Int
+  numbering = do
+    i <- S $ get
+    S $ modify succ
+    return i
+
+-- This example is stolen from one example of bindlib.
+-- https://github.com/rlepigre/ocaml-bindlib/blob/master/examples/pred2.ml
+
+data Symbol = Symbol Text Int
+  deriving (Eq, Show)
+
+data Term
+  = Term'Var (Var S Term)
+  | Term'Fun Symbol [Term]
+
+data Form
+  = Form'Imply Form Form
+  | Form'Univ1 (Binder Term S Form)
+  | Form'Univ2 Int (Binder Pred S Form)
+  | Form'FVari (Var S Pred) [Term]
+
+newtype Pred = Pred { unPred :: BinderList Term S Form }
+
+data Proof
+  = Proof'ImplyI Form (Binder Proof S Proof)
+  | Proof'ImplyE Proof Proof
+  | Proof'Univ1I (Binder Term S Proof)
+  | Proof'Univ1E Proof Term
+  | Proof'Univ2I Int (Binder Pred S Proof)
+  | Proof'Univ2E Proof Pred
+  | Proof'Axiom Form (Var S Proof)
+
+pred'Arity :: Getter Pred Int
+pred'Arity = to unPred . binderList'Arity
+pred'makeRaw :: Box S (BinderList Term S Form) -> Box S Pred
+pred'makeRaw = fmap Pred
+pred'make :: VarList S Term -> Box S Form -> Box S Pred
+pred'make xs t = pred'makeRaw $ bindList xs t
+
+term'mkFree :: Var S Term -> S Term
+term'mkFree = return . Term'Var
+pred'mkFree :: Int -> Var S Pred -> S Pred
+pred'mkFree n vp = do
+  let names = if n == 1 then ["x"]
+                        else flip map [1..n] $ \i -> "x" <> T.pack (show i)
+  xs <- newVarList names term'mkFree
+  let ts = boxList $ map term'Var xs
+      p = Form'FVari vp <$> ts
+  fmap Pred $ unbox $ bindList xs p
+proof'mkFree :: Form -> Var S Proof -> S Proof
+proof'mkFree f = return . Proof'Axiom f
+
+term'Var :: Var S Term -> Box S Term
+term'Var = boxVar
+term'Fun :: Symbol -> [Box S Term] -> Box S Term
+term'Fun s ts = Term'Fun s <$> boxList ts
+form'Imply :: Box S Form -> Box S Form -> Box S Form
+form'Imply f g = Form'Imply <$> f <*> g
+form'Univ1Raw :: Box S (Binder Term S Form) -> Box S Form
+form'Univ1Raw = fmap Form'Univ1
+form'Univ1 :: Var S Term -> Box S Form -> Box S Form
+form'Univ1 x t = form'Univ1Raw $ bind x t
+form'Univ2Raw :: Int -> Box S (Binder Pred S Form) -> Box S Form
+form'Univ2Raw arity = fmap $ Form'Univ2 arity
+form'Univ2 :: Int -> Var S Pred -> Box S Form -> Box S Form
+form'Univ2 arity x t = form'Univ2Raw arity $ bind x t
+form'FVari :: Var S Pred -> [Box S Term] -> Box S Form
+form'FVari x ts = Form'FVari x <$> boxList ts
+proof'ImplyIRaw :: Box S Form -> Box S (Binder Proof S Proof) -> Box S Proof
+proof'ImplyIRaw p b = Proof'ImplyI <$> p <*> b
+proof'ImplyI :: Box S Form -> Var S Proof -> Box S Proof -> Box S Proof
+proof'ImplyI p x t = proof'ImplyIRaw p $ bind x t
+proof'ImplyE :: Box S Proof -> Box S Proof -> Box S Proof
+proof'ImplyE p q = Proof'ImplyE <$> p <*> q
+proof'Univ1IRaw :: Box S (Binder Term S Proof) -> Box S Proof
+proof'Univ1IRaw = fmap Proof'Univ1I
+proof'Univ1I :: Var S Term -> Box S Proof -> Box S Proof
+proof'Univ1I x t = proof'Univ1IRaw $ bind x t
+proof'Univ1E :: Box S Proof -> Box S Term -> Box S Proof
+proof'Univ1E p q = Proof'Univ1E <$> p <*> q
+proof'Univ2IRaw :: Int -> Box S (Binder Pred S Proof) -> Box S Proof
+proof'Univ2IRaw arity = fmap $ Proof'Univ2I arity
+proof'Univ2I :: Int -> Var S Pred -> Box S Proof -> Box S Proof
+proof'Univ2I arity x t = proof'Univ2IRaw arity $ bind x t
+proof'Univ2E :: Box S Proof -> Box S Pred -> Box S Proof
+proof'Univ2E p q = Proof'Univ2E <$> p <*> q
+proof'Axiom :: Box S Form -> Var S Proof -> Box S Proof
+proof'Axiom f v = (\g -> Proof'Axiom g v) <$> f
+
+boxTerm :: Term -> S (Box S Term)
+boxTerm (Term'Var x) = return $ term'Var x
+boxTerm (Term'Fun s ts) = fmap (term'Fun s) $ sequenceA $ boxTerm <$> ts
+boxForm :: Form -> S (Box S Form)
+boxForm (Form'Imply a b) = form'Imply <$> boxForm a <*> boxForm b
+boxForm (Form'Univ1 b) = form'Univ1Raw <$> boxBinder boxForm b
+boxForm (Form'Univ2 a b) = form'Univ2Raw a <$> boxBinder boxForm b
+boxForm (Form'FVari x ts) = do
+  let arg1 = unPred <$> boxVar x
+  arg2 <- fmap boxList $ sequenceA $ boxTerm <$> ts
+  boxJoin $ substList <$> arg1 <*> arg2
+
+showTerm :: Term -> Text
+showTerm (Term'Var x) = nameOf x
+showTerm (Term'Fun (Symbol s _) ts) =
+  s <> "(" <> mconcat (intersperse ", " $ map showTerm ts) <> ")"
+showForm :: Form -> S Text
+showForm (Form'Imply a b) = do
+  sha <- showForm a
+  shb <- showForm b
+  return $ "(" <> sha <> ") => (" <> shb <> ")"
+showForm (Form'Univ1 b) = do
+  (x, t) <- unbind b
+  sht <- showForm t
+  return $ "forall_1 " <> nameOf x <> ".(" <> sht <> ")"
+showForm (Form'Univ2 _ b) = do
+  (x, t) <- unbind b
+  sht <- showForm t
+  return $ "forall_2 " <> nameOf x <> ".(" <> sht <> ")"
+showForm (Form'FVari x ts) = do
+  return $ nameOf x <> "(" <> mconcat (intersperse ", " $ map showTerm ts) <> ")"
+
+eqTerm :: Term -> Term -> Bool
+eqTerm (Term'Var x) (Term'Var y) = x == y
+eqTerm (Term'Fun s1 ts1) (Term'Fun s2 ts2) =
+  s1 == s2 && and (map (uncurry eqTerm) $ zip ts1 ts2)
+eqTerm _ _ = False
+eqForm :: Form -> Form -> S Bool
+eqForm (Form'Imply a1 b1) (Form'Imply a2 b2) = do
+  ca <- eqForm a1 a2
+  cb <- eqForm b1 b2
+  return $ ca && cb
+eqForm (Form'Univ1 b1) (Form'Univ1 b2) = eqBinder eqForm b1 b2
+eqForm (Form'Univ2 a1 b1) (Form'Univ2 a2 b2) = do
+  c <- eqBinder eqForm b1 b2
+  return $ a1 == a2 && c
+eqForm (Form'FVari x1 ts1) (Form'FVari x2 ts2) =
+  return $ x1 == x2 && and (map (uncurry eqTerm) $ zip ts1 ts2)
+eqForm _ _ = return False
+
+data BadProof
+  = BadProof'Imply
+  | BadProof'ImplyDifferForm Form Form
+  | BadProof'Univ1
+  | BadProof'Univ2
+
+showBadProof :: BadProof -> S Text
+showBadProof BadProof'Imply = return "BadProof'Imply"
+showBadProof (BadProof'ImplyDifferForm a b) = do
+  sha <- showForm a
+  shb <- showForm b
+  return $ "BadProof'ImplyDifferForm (" <> sha <> ") (" <> shb <> ")"
+showBadProof BadProof'Univ1 = return "BadProof'Univ1"
+showBadProof BadProof'Univ2 = return "BadProof'Univ2"
+
+typeInfer :: Proof -> S (Either BadProof Form)
+typeInfer = unbox <=< fn
+ where
+  fn :: Proof -> S (Box S (Either BadProof Form))
+  fn (Proof'ImplyI f p) = do
+    ax <- newVar (p ^. binder'Name) $ proof'mkFree f
+    tax <- proof'mkFree f ax
+    pr <- subst p tax
+    ber <- fn pr
+    er <- unbox ber
+    case er of
+      Right r -> do
+        bf <- boxForm f
+        br <- boxForm r
+        return $ Right <$> form'Imply bf br
+      Left err -> return $ pure $ Left err
+  fn (Proof'ImplyE p1 p2) = do
+    mf1' <- unbox =<< fn p2
+    mf2' <- unbox =<< fn p1
+    case (mf1', mf2') of
+      (Right f1', Right (Form'Imply f1 f2)) -> do
+        b <- eqForm f1 f1'
+        if b then fmap Right <$> boxForm f2
+             else return $ pure $ Left $ BadProof'ImplyDifferForm f1 f1'
+      _ -> return $ pure $ Left BadProof'Imply
+  fn (Proof'Univ1I p) = do
+    t <- newVar (p ^. binder'Name) term'mkFree
+    te <- term'mkFree t
+    pr <- subst p te
+    ef <- unbox =<< fn pr
+    case ef of
+      Right f -> do
+        bf <- boxForm f
+        return $ Right <$> form'Univ1 t bf
+      Left err -> return $ pure $ Left err
+  fn (Proof'Univ1E p t) = do
+    mf <- unbox =<< fn p
+    case mf of
+      Right (Form'Univ1 b) -> do
+        f <- subst b t
+        fmap Right <$> boxForm f
+      Right _ -> return $ pure $ Left BadProof'Univ1
+      Left err -> return $ pure $ Left err
+  fn (Proof'Univ2I arity f) = do
+    t <- newVar (f ^. binder'Name) $ pred'mkFree arity
+    pr <- pred'mkFree arity t
+    eg <- unbox =<< fn =<< subst f pr
+    case eg of
+      Right g -> do
+        bg <- boxForm g
+        return $ fmap Right $ form'Univ2 arity t bg
+      Left err -> return $ pure $ Left err
+  fn (Proof'Univ2E p p0) = do
+    mf <- unbox =<< fn p
+    case mf of
+      Right (Form'Univ2 arity b) -> if arity == p0 ^. pred'Arity
+        then do
+          f <- subst b p0
+          fmap Right <$> boxForm f
+        else return $ pure $ Left BadProof'Univ2
+      Right _ -> return $ pure $ Left BadProof'Univ2
+      Left err -> return $ pure $ Left err
+  fn (Proof'Axiom f _) = fmap Right <$> boxForm f
+
+typeCheck :: Proof -> Form -> S Bool
+typeCheck p f0 = do
+  ef <- typeInfer p
+  case ef of
+    Right f -> eqForm f0 f
+    _ -> return False
+
+
+leq :: S (Box S Pred)
+leq = do
+  u <- newVar "u" term'mkFree
+  v <- newVar "v" term'mkFree
+  let bu = term'Var u
+      bv = term'Var v
+  x <- newVar "X" $ pred'mkFree 1
+  let bl = unPred <$> boxVar x
+  p1 <- bindListApply bl $ boxList [bu]
+  p2 <- bindListApply bl $ boxList [bv]
+  return $ fmap Pred $ bindList [u, v] $ form'Univ2 1 x $ form'Imply p1 p2
+
+equalTransitive :: S Form
+equalTransitive = do
+  q <- leq
+  x <- newVar "x" term'mkFree
+  y <- newVar "y" term'mkFree
+  z <- newVar "z" term'mkFree
+  let bx = term'Var x
+      by = term'Var y
+      bz = term'Var z
+      bl = fmap unPred q
+  p1 <- bindListApply bl $ boxList [bx, by]
+  p2 <- bindListApply bl $ boxList [by, bz]
+  p3 <- bindListApply bl $ boxList [bx, bz]
+  unbox $ form'Univ1 x $ form'Univ1 y $ form'Univ1 z $
+    form'Imply p1 $ form'Imply p2 p3
+
+equalTransitiveProof :: S Proof
+equalTransitiveProof = do
+  q <- leq
+  x <- newVar "x" term'mkFree
+  y <- newVar "y" term'mkFree
+  z <- newVar "z" term'mkFree
+  let bx = term'Var x
+      by = term'Var y
+      bz = term'Var z
+      bl = fmap unPred q
+  f <- bindListApply bl $ boxList [bx, by]
+  uf <- unbox f
+  h1 <- newVar "h1" $ proof'mkFree uf
+  g <- bindListApply bl $ boxList [by, bz]
+  ug <- unbox g
+  h2 <- newVar "h2" $ proof'mkFree ug
+  px <- newVar "X" $ pred'mkFree 1
+  p <- bindListApply (unPred <$> boxVar px) $ boxList [bx]
+  up <- unbox p
+  h3 <- newVar "h3" $ proof'mkFree up
+  unbox $ proof'Univ1I x $ proof'Univ1I y $ proof'Univ1I z $
+    proof'ImplyI f h1 $ proof'ImplyI g h2 $
+    proof'Univ2I 1 px $ proof'ImplyI p h3 $
+    proof'ImplyE (proof'Univ2E (boxVar h2) (boxVar px)) $
+    proof'ImplyE (proof'Univ2E (boxVar h1) (boxVar px)) (boxVar h3)
+
+spec :: Spec
+spec = describe "leq" $ do
+  it "forms correctly" $ do
+    let r = "forall_1 x.(forall_1 y.(forall_1 z.((forall_2 X.((X(x)) => (X(y)))) => ((forall_2 X.((X(y)) => (X(z)))) => (forall_2 X.((X(x)) => (X(z))))))))"
+    flip shouldReturn r $ flip evalStateT 0 $ runS $ do
+      f <- equalTransitive
+      showForm f
+  it "infers type soundly" $ do
+    let r = "forall_1 x.(forall_1 y.(forall_1 z.((forall_2 X.((X(x)) => (X(y)))) => ((forall_2 X.((X(y)) => (X(z)))) => (forall_2 X.((X(x)) => (X(z))))))))"
+    flip shouldReturn r $ flip evalStateT 0 $ runS $ do
+      ef <- typeInfer =<< equalTransitiveProof
+      case ef of
+        Right f -> showForm f
+        Left bp -> showBadProof bp
+  it "checks correctly" $ do
+    let r = True
+    flip shouldReturn r $ flip evalStateT 0 $ runS $ do
+      p <- equalTransitiveProof
+      f <- equalTransitive
+      typeCheck p f