diff --git a/Changelog.md b/Changelog.md
--- a/Changelog.md
+++ b/Changelog.md
@@ -1,5 +1,16 @@
 # NEXT
 
+# 0.4.3
+
+* Add an `instantiate` function that substitutes a list of terms for a collection of bound variables in a toplevel `Bind p t` term.
+  Thanks to Stephanie Weirich (sweirich).  This adds a new `substBvs` function to the `Subst` class.
+* Add `substBind` operation that substitutes for the bound variable of a `Bind (Name a) t` term.
+  This is a specialization of `instantiate` to the case where the pattern is a single `Name a`
+* Tests for `substBind` by Mark Lemay (marklemay) Thanks!
+* Expose `Rec` constructor of the `Rec` type and the `ctxLevel` function from `AlphaCtx`
+* Require `transformers < 0.6`, run CI with GHC 9.4, drop CI with GHC 7.10.
+  Thanks to Andreas Abel (andreaasabel).
+
 # 0.4.2
 
 * Add `Functor` instance for `Unbound.Generics.LocallyNameless.Internal.Iso.Exchange`
@@ -117,7 +128,7 @@
 * Tested with GHC 8.2.2
 * Compile with `-Wcompat`
 * Add `Semigroup` instances for all types that were previously `Monoid` instances
-* Added more examples to the [examples/ directory](https://github.com/lambdageek/unbound-generics/tree/master/examples)
+* Added more examples to the [examples/ directory](https://github.com/lambdageek/unbound-generics/tree/main/examples)
 * Added "exceptions" dependency and `MonadThrow`, `MonadCatch`, `MonadMask` instances for `FreshMT` and `LFreshMT`.
   Thanks Alex McKenna.
 
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -4,7 +4,7 @@
 [![Discord](https://img.shields.io/discord/732650960471720076?logo=discord)](https://discord.gg/CRfu93W)
 
 [![Hackage](https://img.shields.io/hackage/v/unbound-generics.svg)](https://hackage.haskell.org/package/unbound-generics)
-[![CI](https://github.com/lambdageek/unbound-generics/workflows/CI/badge.svg)](https://github.com/lambdageek/unbound-generics/actions?query=workflow%3ACI+branch%3Amaster)
+[![CI](https://github.com/lambdageek/unbound-generics/workflows/CI/badge.svg)](https://github.com/lambdageek/unbound-generics/actions?query=workflow%3ACI+branch%3Amain)
 <!-- [![Build Status](https://travis-ci.org/lambdageek/unbound-generics.svg)](https://travis-ci.org/lambdageek/unbound-generics) -->
 
 Support for programming with names and binders using GHC Generics.
@@ -50,18 +50,18 @@
 
 -- evaluation takes an expression and returns a value while using a source of fresh names
 eval :: Expr -> FreshM Expr
-eval (V x) = fail $ "unbound variable " ++ show x
-eval e@(Lam {}) = return e
+eval (V x) = error $ "unbound variable " ++ show x
+eval e@Lam{} = return e
 eval (App e1 e2) = do
   v1 <- eval e1
   v2 <- eval e2
   case v1 of
-   (Lam bnd) -> do
+   Lam bnd -> do
      -- open the lambda by picking a fresh name for the bound variable x in body
      (x, body) <- unbind bnd
      let body' = subst x v2 body
      eval body'
-   _ -> fail "application of non-lambda"
+   _ -> error "application of non-lambda"
 
 example :: Expr
 example =
diff --git a/examples/F.hs b/examples/F.hs
--- a/examples/F.hs
+++ b/examples/F.hs
@@ -26,14 +26,14 @@
 
 data Ty = TyVar TyName
         | Arr Ty Ty
-        | All (Bind TyName Ty)
+        | All (Bind [TyName] Ty)
    deriving (Show, Generic, Typeable)
 
 data Tm = TmVar TmName
         | Lam (Bind (TmName, Embed Ty) Tm)
-        | TLam (Bind TyName Tm)
+        | TLam (Bind [TyName] Tm)
         | App Tm Tm
-        | TApp Tm Ty
+        | TApp Tm [Ty]
    deriving (Show, Generic, Typeable)
 
 ------------------------------------------------------
@@ -65,21 +65,31 @@
 
 -- /\a. \x:a. x
 polyid :: Tm
-polyid = TLam (bind a (Lam (bind (x, Embed (TyVar a)) (TmVar x))))
+polyid = TLam (bind [a] (Lam (bind (x, Embed (TyVar a)) (TmVar x))))
 
 -- All a. a -> a
 polyidty :: Ty
-polyidty = All (bind a (Arr (TyVar a) (TyVar a)))
+polyidty = All (bind [a] (Arr (TyVar a) (TyVar a)))
 
 -- /\b. \y:b. y
 polyid2 :: Tm
-polyid2 = TLam (bind b (Lam (bind (y, Embed (TyVar b)) (TmVar y))))
+polyid2 = TLam (bind [b] (Lam (bind (y, Embed (TyVar b)) (TmVar y))))
 
 -- /\c. \y:b. y
 bad_polyid2 :: Tm
-bad_polyid2 = TLam (bind c (Lam (bind (y, Embed (TyVar b)) (TmVar y))))
+bad_polyid2 = TLam (bind [c] (Lam (bind (y, Embed (TyVar b)) (TmVar y))))
 
+-- /\a b. a -> b -> a
+const_ty :: Ty
+const_ty = All (bind [a,b] (Arr (TyVar a) (Arr (TyVar b) (TyVar a))))
 
+-- /\a b. a -> b -> a
+const_tm :: Tm
+const_tm = TLam (bind [a,b] (Lam (bind (x, Embed (TyVar a)) (Lam (bind (y, Embed (TyVar b)) (TmVar x))))))
+
+test :: Ty
+test = fst (runM (ti emptyCtx (TApp const_tm [polyidty, All (bind [c] (TyVar c))])))
+
 -----------------------------------------------------------------
 -- Typechecker
 -----------------------------------------------------------------
@@ -112,8 +122,8 @@
       Just s -> return s
       Nothing -> throwError "NotFound"
 
-extendTy :: TyName -> Ctx -> Ctx
-extendTy n ctx = ctx { getDelta =  n : (getDelta ctx) }
+extendTy :: [TyName] -> Ctx -> Ctx
+extendTy ns ctx = ctx { getDelta =  ns <> (getDelta ctx) }
 
 extendTm :: TmName -> Ty -> Ctx -> Ctx
 extendTm n ty ctx = ctx { getGamma = (n, ty) : (getGamma ctx) }
@@ -162,9 +172,8 @@
   tyt <- ti g t
   case tyt of
    (All bnder) -> do
-      tcty g  ty
-      (n1, ty1) <- unbind bnder
-      return $ subst n1 ty ty1
+      mapM_ (tcty g) ty
+      return $ instantiate bnder ty
    _ -> throwError $ "Expected a ForAll in a type application, got " ++ show tyt
 
 
diff --git a/examples/LC.hs b/examples/LC.hs
--- a/examples/LC.hs
+++ b/examples/LC.hs
@@ -48,8 +48,7 @@
   e2' <- red e2
   case e1' of
     Lam bnd -> do
-        (x, e1'') <- unbind bnd
-        return $ subst x e2' e1''
+        return $ substBind bnd e2'
     otherwise -> return $ App e1' e2'
 red (Lam bnd) = do
    (x, e) <- unbind bnd
@@ -105,3 +104,4 @@
   assertM "be3" $ if_ true (Var x) (Var y) =~ Var x
   assertM "be4" $ if_ false (Var x) (Var y) =~ Var y
   assertM "be5" $ App (App plus one) two =~ three
+  print "Done"
diff --git a/src/Unbound/Generics/LocallyNameless/Alpha.hs b/src/Unbound/Generics/LocallyNameless/Alpha.hs
--- a/src/Unbound/Generics/LocallyNameless/Alpha.hs
+++ b/src/Unbound/Generics/LocallyNameless/Alpha.hs
@@ -25,6 +25,7 @@
   , NthPatFind(..)
   , NamePatFind(..)
   , AlphaCtx
+  , ctxLevel
   , initialCtx
   , patternCtx
   , termCtx
@@ -32,6 +33,7 @@
   , incrLevelCtx
   , decrLevelCtx
   , isZeroLevelCtx
+  , ctxLevel
   -- * Internal
   , gaeq
   , gfvAny
diff --git a/src/Unbound/Generics/LocallyNameless/Fresh.hs b/src/Unbound/Generics/LocallyNameless/Fresh.hs
--- a/src/Unbound/Generics/LocallyNameless/Fresh.hs
+++ b/src/Unbound/Generics/LocallyNameless/Fresh.hs
@@ -30,7 +30,9 @@
 #endif
 import Control.Monad.Trans
 import Control.Monad.Trans.Except
+#if !MIN_VERSION_transformers(0,6,0)
 import Control.Monad.Trans.Error
+#endif
 import Control.Monad.Trans.Maybe
 import Control.Monad.Trans.Reader
 import Control.Monad.Trans.State.Lazy as Lazy
@@ -119,8 +121,10 @@
     return $ (Fn s n)
   fresh nm@(Bn {}) = return nm
 
+#if !MIN_VERSION_transformers(0,6,0)
 instance (Error e, Fresh m) => Fresh (ErrorT e m) where
   fresh = lift . fresh
+#endif
 
 instance Fresh m => Fresh (ExceptT e m) where
   fresh = lift . fresh
diff --git a/src/Unbound/Generics/LocallyNameless/LFresh.hs b/src/Unbound/Generics/LocallyNameless/LFresh.hs
--- a/src/Unbound/Generics/LocallyNameless/LFresh.hs
+++ b/src/Unbound/Generics/LocallyNameless/LFresh.hs
@@ -77,10 +77,14 @@
 import Control.Applicative (Applicative, Alternative)
 
 import Control.Monad.Trans.Cont
+#if !MIN_VERSION_transformers(0,6,0)
 import Control.Monad.Trans.Error
+#endif
 import Control.Monad.Trans.Except
 import Control.Monad.Trans.Identity
+#if !MIN_VERSION_transformers(0,6,0)
 import Control.Monad.Trans.List
+#endif
 import Control.Monad.Trans.Maybe
 import Control.Monad.Trans.State.Lazy as Lazy
 import Control.Monad.Trans.State.Strict as Strict
@@ -164,10 +168,12 @@
   avoid  = mapContT . avoid
   getAvoids = lift getAvoids
 
+#if !MIN_VERSION_transformers(0,6,0)
 instance (Error e, LFresh m) => LFresh (ErrorT e m) where
   lfresh = lift . lfresh
   avoid  = mapErrorT . avoid
   getAvoids = lift getAvoids
+#endif
 
 instance LFresh m => LFresh (ExceptT e m) where
   lfresh = lift . lfresh
@@ -179,10 +185,12 @@
   avoid  = mapIdentityT . avoid
   getAvoids = lift getAvoids
 
+#if !MIN_VERSION_transformers(0,6,0)
 instance LFresh m => LFresh (ListT m) where
   lfresh = lift . lfresh
   avoid  = mapListT . avoid
   getAvoids = lift getAvoids
+#endif
 
 instance LFresh m => LFresh (MaybeT m) where
   lfresh = lift . lfresh
diff --git a/src/Unbound/Generics/LocallyNameless/Rec.hs b/src/Unbound/Generics/LocallyNameless/Rec.hs
--- a/src/Unbound/Generics/LocallyNameless/Rec.hs
+++ b/src/Unbound/Generics/LocallyNameless/Rec.hs
@@ -13,7 +13,7 @@
 {-# LANGUAGE DeriveGeneric #-}
 module Unbound.Generics.LocallyNameless.Rec
        (
-         Rec
+         Rec (Rec)
        , rec
        , unrec
        , TRec (..)
diff --git a/src/Unbound/Generics/LocallyNameless/Subst.hs b/src/Unbound/Generics/LocallyNameless/Subst.hs
--- a/src/Unbound/Generics/LocallyNameless/Subst.hs
+++ b/src/Unbound/Generics/LocallyNameless/Subst.hs
@@ -46,6 +46,8 @@
   SubstName(..)
   , SubstCoerce(..)
   , Subst(..)
+  , substBind
+  , instantiate
   ) where
 
 import GHC.Generics
@@ -69,6 +71,18 @@
 data SubstCoerce a b where  
   SubstCoerce :: Name b -> (b -> Maybe a) -> SubstCoerce a b
 
+-- | Immediately substitute for the bound variables of a pattern
+-- in a binder, without first naming the variables.
+-- NOTE: this operation does not check that the number of terms passed in
+-- match the number of variables in the pattern. (Or that they are of appropriate type.)
+instantiate :: (Alpha a, Alpha b, Alpha p , Subst a b) => Bind p b -> [a] -> b
+instantiate bnd u = instantiate_ bnd u
+
+-- | A version of 'instantiate' with a more general type
+instantiate_ :: Subst a b => Bind p b -> [a] -> b
+instantiate_ (B _p t) u = substBvs initialCtx u t
+
+
 -- | Instances of @'Subst' b a@ are terms of type @a@ that may contain
 -- variables of type @b@ that may participate in capture-avoiding
 -- substitution.
@@ -109,31 +123,48 @@
     | otherwise =
       error $ "Cannot substitute for bound variable in: " ++ show (map fst ss)
 
+   -- Bound variable substitution (replace a single pattern variable with a list of terms)
+   -- Similar to open, but replaces with b's instead of with names
+   -- Does not check whether enough b's are provided: will ignore extra if there are too many
+   -- and skip the substitution if there are too few.
+  substBvs :: AlphaCtx -> [b] -> a -> a
+  default substBvs :: (Generic a, GSubst b (Rep a)) => AlphaCtx -> [b] -> a -> a
+  substBvs ctx bs x =
+     case (isvar x :: Maybe (SubstName a b)) of
+        Just (SubstName (Bn j k)) | ctxLevel ctx == j, fromInteger k < length bs -> bs !! fromInteger k
+        _ -> to $ gsubstBvs ctx bs (from x)
+
 ---- generic structural substitution.
 
 class GSubst b f where
   gsubst :: Name b -> b -> f c -> f c
   gsubsts :: [(Name b, b)] -> f c -> f c
+  gsubstBvs :: AlphaCtx -> [b] -> f c -> f c
 
 instance Subst b c => GSubst b (K1 i c) where
   gsubst nm val = K1 . subst nm val . unK1
   gsubsts ss = K1 . substs ss . unK1
+  gsubstBvs ctx b = K1 . substBvs ctx b . unK1
 
 instance GSubst b f => GSubst b (M1 i c f) where
   gsubst nm val = M1 . gsubst nm val . unM1
   gsubsts ss = M1 . gsubsts ss . unM1
+  gsubstBvs c b = M1 . gsubstBvs c b . unM1
 
 instance GSubst b U1 where
   gsubst _nm _val _ = U1
   gsubsts _ss _ = U1
+  gsubstBvs _c _b _ = U1
 
 instance GSubst b V1 where
   gsubst _nm _val = id
   gsubsts _ss = id
+  gsubstBvs _c _b = id
 
 instance (GSubst b f, GSubst b g) => GSubst b (f :*: g) where
   gsubst nm val (f :*: g) = gsubst nm val f :*: gsubst nm val g
   gsubsts ss (f :*: g) = gsubsts ss f :*: gsubsts ss g
+  gsubstBvs c b (f :*: g) = gsubstBvs c b f :*: gsubstBvs c b g
 
 instance (GSubst b f, GSubst b g) => GSubst b (f :+: g) where
   gsubst nm val (L1 f) = L1 $ gsubst nm val f
@@ -142,18 +173,21 @@
   gsubsts ss (L1 f) = L1 $ gsubsts ss f
   gsubsts ss (R1 g) = R1 $ gsubsts ss g
 
+  gsubstBvs c b (L1 f) = L1 $ gsubstBvs c b f
+  gsubstBvs c b (R1 g) = R1 $ gsubstBvs c b g
+
 -- these have a Generic instance, but
 -- it's self-refential (ie: Rep Int = D1 (C1 (S1 (Rec0 Int))))
 -- so our structural GSubst instances get stuck in an infinite loop.
-instance Subst b Int where subst _ _ = id ; substs _ = id
-instance Subst b Bool where subst _ _ = id ; substs _ = id
-instance Subst b () where subst _ _ = id ; substs _ = id
-instance Subst b Char where subst _ _ = id ; substs _ = id
-instance Subst b Float where subst _ _ = id ; substs _ = id
-instance Subst b Double where subst _ _ = id ; substs _ = id
+instance Subst b Int where subst _ _ = id ; substs _ = id ; substBvs _ _ = id
+instance Subst b Bool where subst _ _ = id ; substs _ = id ; substBvs _ _ = id
+instance Subst b () where subst _ _ = id ; substs _ = id ; substBvs _ _ = id
+instance Subst b Char where subst _ _ = id ; substs _ = id ; substBvs _ _ = id
+instance Subst b Float where subst _ _ = id ; substs _ = id ; substBvs _ _ = id
+instance Subst b Double where subst _ _ = id ; substs _ = id ; substBvs _ _ = id
 
 -- huh, apparently there's no instance Generic Integer. 
-instance Subst b Integer where subst _ _ = id ; substs _ = id
+instance Subst b Integer where subst _ _ = id ; substs _ = id ; substBvs _ _ = id
 
 instance (Subst c a, Subst c b) => Subst c (a,b)
 instance (Subst c a, Subst c b, Subst c d) => Subst c (a,b,d)
@@ -164,23 +198,41 @@
 instance (Subst c a) => Subst c (Maybe a)
 instance (Subst c a, Subst c b) => Subst c (Either a b)
 
-instance Subst b (Name a) where subst _ _ = id ; substs _ = id
-instance Subst b AnyName where subst _ _ = id ; substs _ = id
+instance Subst b (Name a) where subst _ _ = id  ; substs _ = id ; substBvs _ _ = id
+instance Subst b AnyName where subst _ _ = id ; substs _ = id ; substBvs _ _ = id
 
-instance (Subst c a) => Subst c (Embed a)
+instance (Subst c a) => Subst c (Embed a) where
+  substBvs c us (Embed x)
+    | isTermCtx c = Embed (substBvs (termCtx c) us x)
+    | otherwise = error "Internal error: substBvs on Embed"
 
 instance (Subst c e) => Subst c (Shift e) where
   subst x b (Shift e) = Shift (subst x b e)
   substs ss (Shift e) = Shift (substs ss e)
+  substBvs c b (Shift e) = Shift (substBvs (decrLevelCtx c) b e)
 
-instance (Subst c b, Subst c a, Alpha a, Alpha b) => Subst c (Bind a b)
+instance (Subst c b, Subst c a, Alpha a, Alpha b) => Subst c (Bind a b) where
+  substBvs c b (B p t) = B (substBvs (patternCtx c) b p) (substBvs (incrLevelCtx c) b t)
 
-instance (Subst c p1, Subst c p2) => Subst c (Rebind p1 p2)
+instance (Subst c p1, Subst c p2) => Subst c (Rebind p1 p2) where
+  substBvs c us (Rebnd p q) = Rebnd (substBvs c us p) (substBvs (incrLevelCtx c) us q)
 
-instance (Subst c p) => Subst c (Rec p)
+instance (Subst c p) => Subst c (Rec p) where
+  substBvs c us (Rec p) = Rec (substBvs (incrLevelCtx c) us p)
 
-instance (Alpha p, Subst c p) => Subst c (TRec p)
+instance (Alpha p, Subst c p) => Subst c (TRec p) where
+  substBvs c us (TRec p) = TRec (substBvs (patternCtx (incrLevelCtx c)) us p)
 
 instance Subst a (Ignore b) where
   subst _ _ = id
   substs _ = id
+  substBvs _ _ = id
+
+-- | Specialized version of capture-avoiding substitution for that operates on a @'Bind' ('Name' a) t@ term to @'unbind'@
+-- the bound name @Name a@ and immediately subsitute a new term for its occurrences.
+--
+-- This is a specialization of @'instantiate' :: Bind pat term -> [a] -> term@ where the @'Bind' pat term@ has a pattern that is just
+-- a single @'Name' a@ and there is a single substitution term of type @a@.  Unlike 'instantiate', this function cannot fail at runtime.
+substBind :: Subst a t => Bind (Name a) t -> a -> t
+substBind b u = instantiate_ b [u]
+
diff --git a/test/AlphaProperties.hs b/test/AlphaProperties.hs
new file mode 100644
--- /dev/null
+++ b/test/AlphaProperties.hs
@@ -0,0 +1,27 @@
+module AlphaProperties where
+
+import Unbound.Generics.LocallyNameless (fv, aeq, Name, Alpha)
+
+import Test.Tasty.QuickCheck (counterexample, Property, testProperty)
+
+import Data.Typeable (Typeable)
+
+import Data.Monoid (Any(..))
+import Unbound.Generics.LocallyNameless.Internal.Fold (foldMapOf, toListOf)
+
+
+
+isFreeIn :: (Typeable a, Alpha b) => Name a -> b -> Bool
+isFreeIn = elementOf fv
+  where
+    elementOf l = anyOf l . (==)
+    anyOf l f = getAny . foldMapOf l (Any . f)
+
+notFreeIn :: (Typeable a, Alpha b) => Name a -> b -> Bool
+notFreeIn v = not . isFreeIn v
+
+(=~=) :: (Alpha a, Show a) => a -> a -> Property
+x =~= y = counterexample (show x ++ " not alpha equivalent to " ++ show y) (x `aeq` y)
+
+(/~@) :: (Typeable a, Alpha b, Show b) => Name a -> b -> Property
+v /~@ t = counterexample (show v ++ " is free in " ++ show t) (v `notFreeIn` t)
diff --git a/test/PropOpenClose.hs b/test/PropOpenClose.hs
--- a/test/PropOpenClose.hs
+++ b/test/PropOpenClose.hs
@@ -13,23 +13,8 @@
 import Unbound.Generics.LocallyNameless
 import Unbound.Generics.LocallyNameless.Internal.Fold (foldMapOf, toListOf)
 
-----------------------------------------
--- Property testing utilities
-
-isFreeIn :: (Typeable a, Alpha b) => Name a -> b -> Bool
-isFreeIn = elementOf fv
-  where
-    elementOf l = anyOf l . (==)
-    anyOf l f = getAny . foldMapOf l (Any . f)
-
-notFreeIn :: (Typeable a, Alpha b) => Name a -> b -> Bool
-notFreeIn v = not . isFreeIn v
-
-(=~=) :: (Alpha a, Show a) => a -> a -> Property
-x =~= y = counterexample (show x ++ " not alpha equivalent to " ++ show y) (x `aeq` y)
+import AlphaProperties
 
-(/~@) :: (Typeable a, Alpha b, Show b) => Name a -> b -> Property
-v /~@ t = counterexample (show v ++ " is free in " ++ show t) (v `notFreeIn` t)
 
 -- Wrapper around 'Name a' that has an Arbitrary instance that generates free names.
 -- Note that this doesn't guarantee /freshness/.  The name may clash with some other one.
diff --git a/test/TestSubstBind.hs b/test/TestSubstBind.hs
new file mode 100644
--- /dev/null
+++ b/test/TestSubstBind.hs
@@ -0,0 +1,102 @@
+{-# LANGUAGE MultiParamTypeClasses, DeriveGeneric, DeriveDataTypeable #-}
+
+module TestSubstBind  where
+
+import Test.Tasty
+import Unbound.Generics.LocallyNameless
+import Data.Typeable (Typeable)
+import GHC.Generics (Generic)
+
+
+import Test.QuickCheck
+import Test.Tasty.QuickCheck (testProperty)
+import Unbound.Generics.LocallyNameless.Unsafe (unsafeUnbind)
+
+import AlphaProperties 
+
+type Var = Name Expr
+
+data Expr = V Var | Lam (Bind Var Expr) | I Int | App Expr Expr
+  deriving (Generic, Typeable, Show)
+
+instance Alpha Expr
+
+instance Subst Expr Expr where
+  isvar (V x) = Just (SubstName x)
+  isvar _     = Nothing
+
+
+instance Arbitrary Expr where
+  arbitrary = sized arbitrarySizedExpr
+
+  shrink (I i) = I <$> shrink i
+  shrink (Lam bndExp) = 
+    (substBind bndExp <$> [I 0, V x, V y, V z]) -- does the problem persist with the binder removed?
+     ++ (Lam <$> underBinder shrink bndExp) -- shrink under the binder
+  shrink (f `App` a) = [f, a] ++ (App <$> shrink f <*> shrink a)
+  shrink _ = []
+
+underBinder :: (Monad m) => (Expr -> m Expr) -> Bind Var Expr -> m (Bind Var Expr)
+underBinder op bndExp = let 
+  (name, bod) = unsafeUnbind bndExp -- Should be safe since no freshnames are invoked
+  in do
+    bod' <- op bod
+    pure $ bind name bod'
+
+arbitrarySizedExpr :: Int -> Gen Expr
+arbitrarySizedExpr i | i < 1 = do 
+  n <- arbitrary 
+  var <- elements [x,y,z]
+  elements [I n, V $ var]
+arbitrarySizedExpr i = do 
+  rest <- arbitrarySizedExpr (i - 1)
+  var <- elements [x,y,z]
+  n <- arbitrary 
+  f <- arbitrarySizedExpr (i `div` 2) -- TODO: reorganize better
+  a <- arbitrarySizedExpr (i `div` 2)
+  elements [Lam $ bind var rest, f `App` a, I n, V $ var]
+
+
+x,y,z :: Var
+x = s2n "x"
+y = s2n "y"
+z = s2n "z"
+
+
+smallStep :: Expr -> Maybe Expr
+smallStep ((Lam bndBod) `App` a) = Just $ substBind bndBod a
+smallStep (f `App` a) = 
+  case (smallStep f, smallStep a) of
+    (Nothing, Nothing) -> Nothing
+    (Just f', _) -> Just $ f' `App` a
+    (Nothing, Just a') -> Just $ f `App` a'
+smallStep (Lam bndBod) = Lam <$> underBinder smallStep bndBod
+smallStep _ = Nothing -- no step
+
+
+smallStep' :: (Fresh m) => Expr -> m (Maybe Expr)
+smallStep' ((Lam bndBod) `App` a) = do
+  (name, bod) <- unbind bndBod
+  pure $ Just $ subst name a bod
+smallStep' (f `App` a) = do
+  mf' <- smallStep' f
+  ma' <- smallStep' a
+  case (mf', ma') of
+    (Nothing, Nothing) -> pure $ Nothing
+    (Just f', _) -> pure $ Just $ f' `App` a
+    (Nothing, Just a') -> pure $ Just $ f `App` a'
+smallStep' (Lam bndBod) = do
+  (name, bod) <- unbind bndBod
+  mbod' <- smallStep' bod
+  case mbod' of
+    Nothing -> pure $ Nothing
+    Just bod' -> pure $ Just $ Lam $ bind name bod'
+smallStep' _ = pure $ Nothing -- no step
+
+
+expbindProp ::  Expr -> Property
+expbindProp e = smallStep e =~= runFreshM (smallStep' e)
+
+test_substBind :: TestTree
+test_substBind = testGroup "substBind"
+          [testProperty "substBind matches unbind subst" $ expbindProp]
diff --git a/test/test-main.hs b/test/test-main.hs
--- a/test/test-main.hs
+++ b/test/test-main.hs
@@ -11,6 +11,7 @@
 import TestIgnore
 import TestShiftEmbed
 import TestTH
+import TestSubstBind
 
 main :: IO ()
 main = defaultMain $ testGroup "unboundGenerics"
@@ -24,4 +25,5 @@
        , test_acompare
        , test_shiftEmbed
        , test_TH
+       , test_substBind
        ]
diff --git a/unbound-generics.cabal b/unbound-generics.cabal
--- a/unbound-generics.cabal
+++ b/unbound-generics.cabal
@@ -1,8 +1,6 @@
--- Initial unbound-generics.cabal generated by cabal init.  For further 
--- documentation, see http://haskell.org/cabal/users-guide/
-
+cabal-version:       >=1.10
 name:                unbound-generics
-version:             0.4.2
+version:             0.4.3
 synopsis:            Support for programming with names and binders using GHC Generics
 description:         Specify the binding structure of your data type with an
                      expressive set of type combinators, and unbound-generics
@@ -15,7 +13,7 @@
                      but using <https://hackage.haskell.org/package/base/docs/GHC-Generics.html GHC.Generics>
                      instead of <http://hackage.haskell.org/package/RepLib RepLib>.
                      See the accompanying README for some porting notes.
-                     
+
 homepage:            http://github.com/lambdageek/unbound-generics
 bug-reports:         http://github.com/lambdageek/unbound-generics/issues
 license:             BSD3
@@ -25,12 +23,13 @@
 copyright:           (c) 2014-2022, Aleksey Kliger
 category:            Language
 build-type:          Simple
+
 extra-source-files:  examples/*.hs, examples/*.lhs,
                      README.md,
                      Changelog.md
-cabal-version:       >=1.10
-tested-with: GHC == 7.8.4, GHC == 7.10.3, GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.4, GHC == 8.6.5, GHC == 8.8.3, GHC == 8.10.*, GHC == 9.0.*, GHC == 9.2.*
-             
+
+tested-with: GHC == 7.8.4, GHC == 7.10.3, GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.4, GHC == 8.6.5, GHC == 8.8.4, GHC == 8.10.7, GHC == 9.0.2, GHC == 9.2.*, GHC == 9.4.*
+
 library
   exposed-modules:     Unbound.Generics.LocallyNameless
                        Unbound.Generics.LocallyNameless.Name
@@ -57,7 +56,7 @@
                        template-haskell >= 2.8.0.0,
                        deepseq >= 1.3.0.0,
                        mtl >= 2.1,
-                       transformers >= 0.3,
+                       transformers >= 0.3 && < 0.7,
                        transformers-compat >= 0.3,
                        containers >= 0.5 && < 0.7,
                        contravariant >= 0.5,
@@ -87,6 +86,8 @@
                        TestACompare
                        TestShiftEmbed
                        TestTH
+                       TestSubstBind
+                       AlphaProperties
   build-depends:       base,
                        mtl,
                        tasty,