diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -41,67 +41,67 @@
 
 ### Calculi
 
-1. [Untyped lambda calculus](examples/LC.hs)
+1. [Untyped lambda calculus](https://github.com/sweirich/rebound/blob/main/rebound/examples/LC.hs)
 
    Defines the syntax and substitution functions for the untyped lambda
    calculus. Uses these definitions to implement several interpreters.
 
-2. [Untyped lambda calculus with let rec and nested lets](examples/LCLet.hs)
+2. [Untyped lambda calculus with let rec and nested lets](https://github.com/sweirich/rebound/blob/main/rebound/examples/LCLet.hs)
 
    Example of advanced binding forms: recursive definitions and sequenced
    definitions.
 
-3. [Untyped lambda calculus with pattern matching](examples/Pat.hs)
+3. [Untyped lambda calculus with pattern matching](https://github.com/sweirich/rebound/blob/main/rebound/examples/Pat.hs)
 
    Extends the lambda calculus example with pattern matching.
 
-4. [System F](examples/SystemF.hs)
+4. [System F](https://github.com/sweirich/rebound/blob/main/rebound/examples/SystemF.hs)
 
    Working with two separate scopes (type and term variables) is tricky. This
    example shows one way to do it.
 
-5. [Pure System F](examples/PureSystemF.hs)
+5. [Pure System F](https://github.com/sweirich/rebound/blob/main/rebound/examples/PureSystemF.hs)
 
    An alternative way of defining System F, using one single syntactic class.
    Also demonstrates how to use the `ScopedReader` monad for typechecking and
    pretty-printing.
 
-6. [Simple implementation of dependent types](examples/PTS.hs)
+6. [Simple implementation of dependent types](https://github.com/sweirich/rebound/blob/main/rebound/examples/PTS.hs)
 
    An implementation of a simple type checker for a dependent-type system.
    Language includes Pi and Sigma types.
 
-7. [Dependent Pattern Matching](examples/DepMatch.hs)
+7. [Dependent Pattern Matching](https://github.com/sweirich/rebound/blob/main/rebound/examples/DepMatch.hs)
 
    A dependent type system with nested, dependent pattern matching. Patterns may
    also include scoped terms.
 
-8. [Linear Lambda Calculus](examples/LinLC.hs)
+8. [Linear Lambda Calculus](https://github.com/sweirich/rebound/blob/main/rebound/examples/LinLC.hs)
 
    A linear version of the (simply typed) lambda calculus. Demonstrates how to
    thread a typing context using the `ScopedState` monad.
 
 ### Working with well-scoped expressions
 
-1. [Scope checking](examples/ScopeCheck.hs)
+1. [Scope checking](https://github.com/sweirich/rebound/blob/main/rebound/examples/ScopeCheck.hs)
 
    Demonstrates how to convert a "named" (or _nominal_) expression to a
    well-scoped expression.
 
-2. [QuickCheck](examples/LCQC.hs)
+2. [QuickCheck](https://github.com/sweirich/rebound/blob/main/rebound/examples/LCQC.hs)
 
    Demonstrates the use of well-scoped terms with
    [QuickCheck](https://hackage.haskell.org/package/QuickCheck).
 
-3. [HOAS](examples/HOAS.hs)
+3. [HOAS](https://github.com/sweirich/rebound/blob/main/rebound/examples/HOAS.hs)
 
    Demonstrates how to layer a HOAS representation on top of a de Bruijn
    representation. Based on Conor McBride's ["Classy
    Hack"](https://mazzo.li/epilogue/index.html%3Fp=773.html).
 
-4. [PatGen](examples/PatGen.hs)
+4. [PatGen](https://github.com/sweirich/rebound/blob/main/rebound/examples/PatGen.hs)
 
-   A variant of the [Pat](examples/Pat.hs) example, which demonstrates how
+   A variant of the [Pat](https://github.com/sweirich/rebound/blob/main/rebound/examples/Pat.hs) example, which demonstrates how
    generic programming can be used to derive some definitions.
 
 ## Related libraries
@@ -130,6 +130,3 @@
   rename the bound variable in abstraction if it is already in the current
   scope.
 
-- [binder](https://hackage.haskell.org/package/binder)
-
-  Uses HOAS.
diff --git a/examples/DepMatch.hs b/examples/DepMatch.hs
--- a/examples/DepMatch.hs
+++ b/examples/DepMatch.hs
@@ -223,22 +223,6 @@
   freeVars (PAnnot p t) = freeVars p <> freeVars t
 
 ----------------------------------------------
--- weakening (convenience functions)
-----------------------------------------------
-
--- >>> :t weaken' s1 t00
--- weaken' s1 t00 :: Exp ('S ('S N1))
-
--- >>> weaken' s1 t00
--- 0 0
-
-weaken' :: SNat m -> Exp n -> Exp (m + n)
-weaken' m = applyE @Exp (weakenE' m)
-
-weakenBind' :: SNat m -> Bind1 Exp Exp n -> Bind1 Exp Exp (m + n)
-weakenBind' m = applyE @Exp (weakenE' m)
-
-----------------------------------------------
 -- strengthening
 ----------------------------------------------
 
@@ -324,6 +308,28 @@
 -- >>> tmid
 -- λ_. (λ_. 0)
 
+sigmaExample :: Exp (S Z)
+sigmaExample = Sigma star (bind1 (Sigma (Var f1) (bind1 (Var f1))))
+
+tyEx = Pi star (bind1 (Pi sigmaExample (bind1 (Var f1))))
+
+-- >>> :t Pat.bind
+-- Pat.bind :: (Sized pat, Subst v c) => pat -> c (Size pat + n) -> Bind v c pat n
+
+tmEx :: Exp Z
+tmEx = Match (Branch (Scoped.bind PVar
+                (Match (Branch (Scoped.bind (PPair PVar (PPair PVar PVar))
+                          (Var f1)) :< Nil))) :< Nil)
+
+-- >>> tyEx
+-- Pi *. (Sigma *. 1 * 1) -> 1
+
+-- >>> tmEx 
+-- λ_. (λ(_, (_, _)). 1)
+
+-- >>> (checkType zeroE tmEx tyEx :: Either Err ())
+-- Right ()
+
 --------------------------------------------------------
 
 -- * Show instances
@@ -602,10 +608,10 @@
   case axiomAssoc @p2 @p1 @n of
     Refl -> do
       (g', e1) <- checkPattern g p1 tyA
-      let tyB' = weakenBind' (size p1) tyB
+      let tyB' = shift (size p1) tyB
       let tyB'' = whnf (instantiate1 tyB' e1)
       (g'', e2) <- checkPattern g' p2 tyB''
-      let e1' = weaken' (size p2) e1
+      let e1' = shift (size p2) e1
       return (g'', Pair e1' e2)
 checkPattern g p ty = do
   (g', e, ty') <- inferPattern g p
diff --git a/examples/PTS.hs b/examples/PTS.hs
--- a/examples/PTS.hs
+++ b/examples/PTS.hs
@@ -66,15 +66,6 @@
 -- False
 instance FV Exp where
 
--- >>> :t weaken' s1 t00
--- weaken' s1 t00 :: Exp ('S ('S N1))
-
--- >>> weaken' s1 t00
--- 0 0
-
-weaken' :: SNat m -> Exp n -> Exp (m + n)
-weaken' m = applyE @Exp (weakenE' m)
-
 -- >>> strengthenRec s1 s1 snat t00
 -- Just (0 0)
 
diff --git a/rebound.cabal b/rebound.cabal
--- a/rebound.cabal
+++ b/rebound.cabal
@@ -1,12 +1,12 @@
 cabal-version:  3.0
 name:           rebound
-version:        0.1.1.0
+version:        0.1.2.0
 description:    Please see the README on GitHub at <https://github.com/sweirich/rebound>
 homepage:       https://github.com/sweirich/rebound
 bug-reports:    https://github.com/sweirich/rebound/issues
 author:         Stephanie Weirich, Noe De Santo
 maintainer:     sweirich@seas.upenn.edu, ndesanto@seas.upenn.edu
-copyright:      2025 Stephanie Weirich, Noe De Santo
+copyright:      2026 Stephanie Weirich, Noe De Santo
 license:        MIT
 license-file:   LICENSE
 build-type:     Simple
@@ -20,6 +20,7 @@
   ghc-options:
      -Wno-type-defaults
      -Wincomplete-patterns
+     -Wno-deprecations
   default-language:
     GHC2021
   default-extensions:
@@ -42,13 +43,13 @@
   import:
       common-stanza
   build-depends:
-      base >= 4.15 && < 5.0
-    , QuickCheck >= 2.15.0.1 && < 2.16
-    , containers >= 0.6.8 && < 0.7
-    , deepseq >= 1.5.1 && < 1.6
+      base >= 4.15 && < 5
+    , containers >= 0.6.7 && < 0.8
+    , deepseq >= 1.4.8 && < 1.6
+    , fin >= 0.3 && < 0.4
     , mtl >= 2.3.1 && < 2.4
-    , fin >= 0.3.2 && < 0.4
-    , vec >= 0.5.1 && < 0.6
+    , QuickCheck >= 2.14.3 && < 2.16
+    , vec >= 0.5 && < 0.6
   exposed-modules:
       Rebound
     , Rebound.Classes
@@ -61,6 +62,7 @@
     , Rebound.Env.StrictA
     , Rebound.Env.StrictB
     , Rebound.Env.Functional
+    , Rebound.Env.ShiftList
     , Rebound.Generics
     , Rebound.Lib
     , Rebound.MonadNamed
@@ -80,6 +82,32 @@
     , Data.Scoped.Classes
     , Data.Scoped.Maybe
   hs-source-dirs: src
+
+library rebound-examples
+  import:
+    common-stanza
+  visibility: private
+  build-depends:
+    base >=4.15, base < 5
+    , rebound
+    , mtl
+    , HUnit < 1.7
+    , QuickCheck
+    , containers
+    , prettyprinter < 1.8
+  exposed-modules:
+      LC
+    , LCQC
+    , LCLet
+    , PTS
+    , Pat
+    , DepMatch
+    , ScopeCheck
+    , HOAS
+    , SystemF
+    , PureSystemF
+    , LinLC
+  hs-source-dirs: examples
 
 test-suite rebound-tests
   import:
diff --git a/src/Data/Fin.hs b/src/Data/Fin.hs
--- a/src/Data/Fin.hs
+++ b/src/Data/Fin.hs
@@ -23,6 +23,7 @@
   invert,
   shiftN,
   shift1,
+  split,
   weakenFin,
   weakenFinRight,
   weaken1Fin,
@@ -236,3 +237,4 @@
   -- Case: x < k, leave it alone
 strengthenRecFin (snat_ -> SS_ k) m n (FS x) =
     FS <$> strengthenRecFin k m n x
+
diff --git a/src/Data/LocalName.hs b/src/Data/LocalName.hs
--- a/src/Data/LocalName.hs
+++ b/src/Data/LocalName.hs
@@ -3,17 +3,31 @@
 -- Description : Strings with an "identity" equality
 module Data.LocalName where
 
+import Test.QuickCheck
+
 -- | A simple wrapper for strings
--- All local names are equal so that when they are used as patterns
+-- All local names are *equal* so that when they are used as patterns
 -- they will be ignored.
 newtype LocalName = LocalName {name :: String}
 
 instance Eq LocalName where
   x1 == x2 = True
 
+rawEq :: LocalName -> LocalName -> Bool
+rawEq n1 n2 = name n1 == name n2
+
 instance Show LocalName where
   show (LocalName x) = x
 
--- | A default name.
+-- | A default name
 internalName :: LocalName
 internalName = LocalName "_internal"
+
+wildcardName :: LocalName
+wildcardName = LocalName "_"
+
+instance Arbitrary LocalName where
+  arbitrary = do 
+    str <- elements [ "x", "y", "z", "w" ]
+    num <- elements [1,2,3,4,5,0]
+    return (LocalName (str ++ show num))
diff --git a/src/Data/Scoped/Classes.hs b/src/Data/Scoped/Classes.hs
--- a/src/Data/Scoped/Classes.hs
+++ b/src/Data/Scoped/Classes.hs
@@ -78,7 +78,7 @@
     maximum x = F.maximum @k (coerce x)
 
     minimum :: (Ord (a n)) => f a n -> a n
-    minimum x = F.maximum @k (coerce x)
+    minimum x = F.minimum @k (coerce x)
 
     sum :: (Num (a n)) => f a n -> a n
     sum x = F.sum @k (coerce x)
diff --git a/src/Data/Scoped/Maybe.hs b/src/Data/Scoped/Maybe.hs
--- a/src/Data/Scoped/Maybe.hs
+++ b/src/Data/Scoped/Maybe.hs
@@ -2,7 +2,7 @@
 -- Module: Data.Scoped.Maybe
 -- Description : Scoped maybe
 --
--- This module defines a Maybe type indexed by a scope
+-- This module defines a Maybe type indexed by a scope.
 -- This module should be imported qualified. Many of the operations
 -- in this module have the same name as prelude functions.
 {-# LANGUAGE DeriveAnyClass #-}
diff --git a/src/Rebound/Bind/Local.hs b/src/Rebound/Bind/Local.hs
--- a/src/Rebound/Bind/Local.hs
+++ b/src/Rebound/Bind/Local.hs
@@ -1,11 +1,15 @@
 -- |
--- Module       : Rebound.Bind.Single
+-- Module       : Rebound.Bind.Local
 -- Description  : Bind a single variable, with a name
 --
--- Single variable binder, but includes a name (represented by a 'LocalName') for pretty printing.
+-- Binders that includes a name (represented by a 'LocalName') for pretty printing.
 -- This is a specialization of "Rebound.Bind.Pat".
 module Rebound.Bind.Local
   ( module Rebound,
+    module Data.Vec,
+    module Data.LocalName,
+
+    -- * Single binder --
     type Bind,
     bind,
     getLocalName,
@@ -17,14 +21,59 @@
     applyUnder,
     bindWith,
     unbindWith,
-    instantiateWith
+    instantiateWith,
+
+-- * single binder --
+    Bind1 (..),
+    bind1,
+    unbind1,
+    unbindl1,
+    getBody1,
+    instantiate1,
+    bindWith1,
+    unbindWith1,
+    instantiateWith1,
+    applyUnder1,
+
+    -- * Double binder --
+    Bind2 (..),
+    bind2,
+    unbind2,
+    getBody2,
+    getLocalName2,
+    instantiate2,
+    bindWith2,
+    unbindWith2,
+    instantiateWith2,
+    applyUnder2,
+
+    -- * N-ary binder ---
+    BindN (..),
+    bindN,
+    unbindN,
+    unbindlN,
+    getBodyN,
+    getLocalNameN,
+    instantiateN,
+    bindWithN,
+    unbindWithN,
+    instantiateWithN,
+    applyUnderN,
   )
 where
 
+import Data.Fin qualified as Fin
+import Data.Vec qualified as Vec
+import Data.Vec (Vec(..))
+import Data.LocalName
 import Rebound
 import Rebound.Bind.Pat qualified as Pat
-import Data.Fin qualified as Fin
+import Rebound.Env qualified as Env
 
+
+
+-- * -- Single Binder
+
 -- | Type binding a single variable.
 -- This data structure includes a delayed
 -- substitution for the variables in the body of the binder.
@@ -81,6 +130,191 @@
 -- The delayed substitution is __not__ applied, but is passed to the function instead.
 instantiateWith :: (SubstVar v) => Bind v c n -> v n -> (forall m. Env v m n -> c m -> c n) -> c n
 instantiateWith b v = Pat.instantiateWith b (oneE v)
+
+
+-- | Type binding a single variable.
+-- This data structure includes a delayed
+-- substitution for the variables in the body of the binder.
+type Bind1 v c n = Bind v c n
+
+-- | Bind a variable, using the identity substitution.
+bind1 :: (Subst v c) => LocalName -> c (S n) -> Bind1 v c n
+bind1 = bind
+
+-- | Bind a variable, while suspending the provided substitution.
+bindWith1 :: forall v c m n. LocalName -> Env v m n -> c (S m) -> Bind1 v c n
+bindWith1 = bindWith
+
+-- | Bind the default \"internal\" variable, while suspending the provided substitution.
+internalBind1 :: (Subst v c) => c (S n) -> Bind1 v c n
+internalBind1 = internalBind
+
+-- | Retrieve the name of the bound variable.
+getLocalName1 :: Bind1 v c n -> LocalName
+getLocalName1 = getLocalName
+
+-- | Retrieve the body of the binding.
+getBody1 :: (Subst v c) => Bind1 v c n -> c (S n)
+getBody1 = getBody
+
+-- | Run a function on the body (and bound name), after applying the delayed substitution.
+unbind1 :: (Subst v c) => Bind1 v c n -> ((LocalName, c (S n)) -> d) -> d
+unbind1 = unbind
+
+-- | Retrieve the body, as well as the bound name.
+unbindl1 :: (Subst v c) => Bind1 v c n -> (LocalName, c (S n))
+unbindl1 = unbindl
+
+-- | Instantiate the body (i.e. replace the bound variable) with the provided term.
+instantiate1 :: (Subst v c) => Bind1 v c n -> v n -> c n
+instantiate1 = instantiate 
+
+-- | Apply a function under the binder.
+-- The delayed substitution is __not__ applied, but is passed to the function instead.
+applyUnder1 ::
+  (Subst v c) =>
+  (forall m. Env v m (S n2) -> c m -> c (S n2)) ->
+  Env v n1 n2 ->
+  Bind1 v c n1 ->
+  Bind1 v c n2
+applyUnder1 = applyUnder
+
+-- | Run a function on the body.
+-- The delayed substitution is __not__ applied, but is passed to the function instead.
+unbindWith1 :: (SubstVar v) => Bind1 v c n -> (forall m. LocalName -> Env v m n -> c (S m) -> d) -> d
+unbindWith1 = unbindWith
+
+-- | Instantiate the body (i.e. replace the bound variable) with the provided term.
+-- The delayed substitution is __not__ applied, but is passed to the function instead.
+instantiateWith1 :: (SubstVar v) => Bind1 v c n -> v n -> (forall m. Env v m n -> c m -> c n) -> c n
+instantiateWith1 = instantiateWith
+
+
+
+-- * -- Double Binder
+
+-- | Type binding a single variable.
+-- This data structure includes a delayed
+-- substitution for the variables in the body of the binder.
+type Bind2 v c n = Pat.Bind v c (Vec N2 LocalName) n
+
+-- | Bind a variable, using the identity substitution.
+bind2 :: (Subst v c) => LocalName -> LocalName -> c (S (S n)) -> Bind2 v c n
+bind2 x y = Pat.bind (x ::: (y ::: VNil))
+
+-- | Bind a variable, while suspending the provided substitution.
+bindWith2 :: forall v c m n. LocalName -> LocalName -> Env v m n -> c (S (S m)) -> Bind2 v c n
+bindWith2 x y = Pat.bindWith (x ::: (y ::: VNil))
+
+-- | Bind the default \"internal\" variable, while suspending the provided substitution.
+internalBind2 :: (Subst v c) => c (S (S n)) -> Bind2 v c n
+internalBind2 = Pat.bind (internalName ::: internalName ::: VNil)
+
+-- | Retrieve the names of the bound variable.
+getLocalName2 :: Bind2 v c n -> Vec N2 LocalName
+getLocalName2 = Pat.getPat
+
+-- | Retrieve the body of the binding.
+getBody2 :: (Subst v c) => Bind2 v c n -> c (S (S n))
+getBody2 = Pat.getBody
+
+-- | Run a function on the body (and bound name), after applying the delayed substitution.
+unbind2 :: (Subst v c) => Bind2 v c n -> ((Vec N2 LocalName, c (S (S n))) -> d) -> d
+unbind2 b f = f (getLocalName2 b, getBody2 b)
+
+-- | Retrieve the body, as well as the bound name.
+unbindl2 :: (Subst v c) => Bind2 v c n -> (Vec N2 LocalName, c (S (S n)))
+unbindl2 b = (getLocalName2 b, getBody2 b)
+
+-- | Instantiate the body (i.e. replace the bound variable) with the provided term.
+instantiate2 :: (Subst v c) => Bind2 v c n -> v n -> v n -> c n
+instantiate2 b e1 e2 = Pat.instantiate b (e1 .: (e2 .: zeroE))
+
+-- | Apply a function under the binder.
+-- The delayed substitution is __not__ applied, but is passed to the function instead.
+applyUnder2 ::
+  (Subst v c) =>
+  (forall m. Env v m (S (S n2)) -> c m -> c (S (S n2))) ->
+  Env v n1 n2 ->
+  Bind2 v c n1 ->
+  Bind2 v c n2
+applyUnder2 = Pat.applyUnder
+
+-- | Run a function on the body.
+-- The delayed substitution is __not__ applied, but is passed to the function instead.
+unbindWith2 :: (SubstVar v) => Bind2 v c n -> 
+   (forall m. LocalName -> LocalName -> Env v m n -> c (S (S m)) -> d) -> d
+unbindWith2 b f = Pat.unbindWith b (\ v e b2 -> f (v Vec.! FZ) (v Vec.! (FS FZ)) e b2)
+
+-- | Instantiate the body (i.e. replace the bound variable) with the provided term.
+-- The delayed substitution is __not__ applied, but is passed to the function instead.
+instantiateWith2 :: (SubstVar v) => 
+  Bind2 v c n -> v n -> v n -> (forall m. Env v m n -> c m -> c n) -> c n
+instantiateWith2 b v1 v2 = Pat.instantiateWith b (v1 .: (v2 .: zeroE))
+
+
+type BindN v c m n = Pat.Bind v c (Vec m LocalName) n
+
+
+-- | Bind a number of variables, using the identity substitution.
+bindN :: forall m v c n. (Subst v c, SNatI m) => Vec m LocalName -> c (m + n) -> BindN v c m n
+bindN = Pat.bind 
+
+-- | Bind a number of variables, while suspending the provided substitution.
+bindWithN :: forall p v c m n. (SNatI p) => Vec p LocalName -> Env v m n -> c (p + m) -> BindN v c p n
+bindWithN = Pat.bindWith 
+
+-- | Run a function on the body, after applying the delayed substitution.
+unbindN :: forall m v c n d. (Subst v c, SNatI n, SNatI m) => 
+   BindN v c m n -> ((SNatI (m + n)) => Vec m LocalName -> c (m + n) -> d) -> d
+unbindN bnd f = Pat.unbind bnd f
+
+-- | Retrieve the body of the binding.
+-- For this kind of binding, it is equivalent to 'getBodyN'.
+unbindlN :: forall m v c n. (Subst v c, SNatI m) => BindN v c m n -> c (m + n)
+unbindlN = Pat.getBody
+
+-- | Retrieve the body of the binding.
+getBodyN :: forall m v c n. (Subst v c, SNatI m) => BindN v c m n -> c (m + n)
+getBodyN = Pat.getBody
+
+getLocalNameN :: BindN v c m n -> Vec m LocalName
+getLocalNameN = Pat.getPat
+
+-- | Instantiate the body (i.e. replace the bound variables) with the provided terms.
+instantiateN :: (Subst v c, SNatI m) => BindN v c m n -> Vec m (v n) -> c n
+instantiateN b v = Pat.instantiate b (fromVec v)
+
+-- | Run a function on the body.
+-- The delayed substitution is __not__ applied, but is passed to the function instead.
+unbindWithN ::
+  (SubstVar v, SNatI m) =>
+  BindN v c m n ->
+  (forall m1. Env v m1 n -> c (m + m1) -> d) ->
+  d
+unbindWithN b f = Pat.unbindWith b (const f)
+
+-- | Instantiate the body (i.e. replace the bound variable) with the provided terms.
+-- The delayed substitution is __not__ applied, but is passed to the function instead.
+instantiateWithN ::
+  forall m v c d n.
+  (SubstVar v, SNatI n, SNatI m) =>
+  BindN v c m n ->
+  Vec m (v n) ->
+  (forall m. Env v m n -> c m -> d n) ->
+  d n
+instantiateWithN b v f =
+  unbindWithN b (f . appendE (snat @m) (fromVec v))
+
+-- | Apply a function under the binder.
+-- The delayed substitution is __not__ applied, but is passed to the function instead.
+applyUnderN ::
+  (Subst v c2, SNatI k) =>
+  (forall m. Env v m (k + n2) -> c1 m -> c2 (k + n2)) ->
+  Env v n1 n2 ->
+  BindN v c1 k n1 ->
+  BindN v c2 k n2
+applyUnderN = Pat.applyUnder
 
 
 -- Example
diff --git a/src/Rebound/Bind/Pat.hs b/src/Rebound/Bind/Pat.hs
--- a/src/Rebound/Bind/Pat.hs
+++ b/src/Rebound/Bind/Pat.hs
@@ -188,7 +188,7 @@
   appearsFree n (Rebind p1 p2) = appearsFree (Fin.shiftN (size p1) n) p2
 
   freeVars :: (Sized p1, FV p2) => Rebind p1 p2 n -> Set (Fin n)
-  freeVars = undefined
+  freeVars (Rebind p1 p2) = rescope (size p1) (freeVars p2)
 
 instance (Sized p1, Strengthen p2) => Strengthen (Rebind p1 p2) where
   strengthenRec (k :: SNat k) (m :: SNat m) (n :: SNat n) (Rebind (p1 :: p1) p2) =
@@ -235,12 +235,3 @@
     Refl <- patEq ps1 ps2
     return Refl
   patEq _ _ = Nothing
-
--- instance
---   (forall p n. WithData v (pat p) n) =>
---   WithData v (PatList pat p) n
---   where
---   extendWithData PNil = id
---   extendWithData (PCons (p1 :: pat p1') (ps :: PatList pat ps')) =
---     case axiomAssoc @ps' @p1' @n of
---       Refl -> extendWithData @v ps . extendWithData @v p1
diff --git a/src/Rebound/Bind/PatN.hs b/src/Rebound/Bind/PatN.hs
--- a/src/Rebound/Bind/PatN.hs
+++ b/src/Rebound/Bind/PatN.hs
@@ -9,6 +9,19 @@
 
     PatN(..),
 
+    -- * single binder (no suffix) --
+    Bind (..),
+    bind,
+    unbind,
+    unbindl,
+    getBody,
+    instantiate,
+    bindWith,
+    unbindWith,
+    instantiateWith,
+    applyUnder,
+
+
     -- * single binder --
     Bind1 (..),
     bind1,
@@ -52,8 +65,6 @@
 import Data.Fin qualified as Fin
 import Data.Vec qualified as Vec
 
-
-
 ----------------------------------------------------------------
 -- N-ary patterns
 ----------------------------------------------------------------
@@ -204,6 +215,81 @@
   Bind1 v c1 n1 ->
   Bind1 v c2 n2
 applyUnder1 = Pat.applyUnder
+
+
+----------------------------------------------------------------
+-- Single binder (other names)
+----------------------------------------------------------------
+
+-- | Type binding 1 variable.
+-- This data structure includes a delayed
+-- substitution for the variables in the body of the binder.
+type Bind v c n = Bind1 v c n 
+
+-- | Bind 1 variable, using the identity substitution.
+bind :: (Subst v c) => c (S n) -> Bind v c n
+bind = bind1
+
+-- | Bind 1 variable, while suspending the provided substitution.
+bindWith :: forall v c m n. Env v m n -> c (S m) -> Bind v c n
+bindWith = bindWith1
+
+-- | Run a function on the body, after applying the delayed substitution.
+unbind ::
+  forall v c n d.
+  (SNatI n, Subst v c) =>
+  Bind v c n ->
+  ((SNatI (S n)) => c (S n) -> d) ->
+  d
+unbind = unbind1
+
+-- | Retrieve the body of the binding.
+-- For this kind of binding, it is equivalent to 'getBody1'.
+unbindl :: forall v c n. (Subst v c) => Bind v c n -> c (S n)
+unbindl = unbindl1
+
+-- | Retrieve the body of the binding.
+getBody ::
+  forall v c n.
+  (Subst v c) =>
+  Bind1 v c n ->
+  c (S n)
+getBody = getBody1
+
+-- | Instantiate the body (i.e. replace the bound variable) with the provided term.
+instantiate :: (Subst v c) => Bind v c n -> v n -> c n
+instantiate = instantiate1
+
+-- | Run a function on the body.
+-- The delayed substitution is __not__ applied, but is passed to the function instead.
+unbindWith ::
+  (SubstVar v) =>
+  Bind v c n ->
+  (forall m. Env v m n -> c (S m) -> d) ->
+  d
+unbindWith = unbindWith1
+
+-- | Instantiate the body (i.e. replace the bound variable) with the provided terms.
+-- The delayed substitution is __not__ applied, but is passed to the function instead.
+instantiateWith ::
+  (SubstVar v) =>
+  Bind v c n ->
+  v n ->
+  (forall m. Env v m n -> c m -> d n) ->
+  d n
+instantiateWith = instantiateWith1
+
+
+-- | Apply a function under the binder.
+-- The delayed substitution is __not__ applied, but is passed to the function instead.
+applyUnder ::
+  (Subst v c2) =>
+  (forall m. Env v m (S n2) -> c1 m -> c2 (S n2)) ->
+  Env v n1 n2 ->
+  Bind v c1 n1 ->
+  Bind v c2 n2
+applyUnder = applyUnder1
+
 
 ----------------------------------------------------------------
 -- Double binder
diff --git a/src/Rebound/Bind/Single.hs b/src/Rebound/Bind/Single.hs
--- a/src/Rebound/Bind/Single.hs
+++ b/src/Rebound/Bind/Single.hs
@@ -22,49 +22,3 @@
 import Rebound
 import Rebound.Bind.PatN
 import Rebound.Classes
-
--- | Type binding a single variable.
--- This data structure includes a delayed
--- substitution for the variables in the body of the binder.
-type Bind v c n = Bind1 v c n
-
--- | Bind a variable, using the identity substitution.
-bind :: (Subst v c) => c (S n) -> Bind v c n
-bind = bind1
-
--- | Bind a variable, while suspending the provided substitution.
-bindWith :: forall v c m n. Env v m n -> c (S m) -> Bind v c n
-bindWith = bindWith1
-
--- | Run a function on the body, after applying the delayed substitution.
-unbind :: forall v c n d. (SNatI n, Subst v c) => Bind v c n -> ((SNatI (S n)) => c (S n) -> d) -> d
-unbind = unbind1
-
--- | Retrieve the body of the binding.
--- For this kind of binding, it is equivalent to 'getBody'.
-unbindl :: (Subst v c) => Bind v c n -> c (S n)
-unbindl = unbindl1
-
--- | Retrieve the body of the binding.
-getBody :: forall v c n. (Subst v c) => Bind v c n -> c (S n)
-getBody = getBody1
-
--- | Instantiate the body (i.e. replace the bound variable) with the provided term.
-instantiate :: (Subst v c) => Bind v c n -> v n -> c n
-instantiate = instantiate1
-
--- | Run a function on the body.
--- The delayed substitution is __not__ applied, but is passed to the function instead.
-unbindWith :: (SubstVar v) => Bind v c n -> (forall m. Env v m n -> c (S m) -> d) -> d
-unbindWith = unbindWith1
-
--- | Instantiate the body (i.e. replace the bound variable) with the provided term.
--- The delayed substitution is __not__ applied, but is passed to the function instead.
-instantiateWith :: (SubstVar v) => Bind v c n -> v n -> (forall m. Env v m n -> c m -> d n) -> d n
-instantiateWith = instantiateWith1
-
--- | Apply a function under the binder.
--- The delayed substitution is __not__ applied, but is passed to the function instead.
-applyUnder :: (Subst v c2) => (forall m. Env v m (S n2) -> c1 m -> c2 (S n2)) -> Env v n1 n2 -> Bind v c1 n1 -> Bind v c2 n2
-applyUnder = applyUnder1
-
diff --git a/src/Rebound/Env.hs b/src/Rebound/Env.hs
--- a/src/Rebound/Env.hs
+++ b/src/Rebound/Env.hs
@@ -38,9 +38,9 @@
     toVec,
     tabulate,
     fromTable,
-    weakenE',
     weakenER,
     shiftFromApplyE,
+    skip
   )
 where
 
@@ -84,8 +84,10 @@
 idE :: (SubstVar v) => Env v n n
 idE = shiftNE s0
 
--- | Append two environments.
---
+
+
+
+-- | append two environments
 -- The `SNatI` constraint is a runtime witness for the length
 -- of the domain of the first environment.
 (.++) ::
@@ -124,10 +126,14 @@
 shift1E :: (SubstVar v) => Env v n (S n)
 shift1E = shiftNE s1
 
--- | Increment all free variables by @p@.
+-- | rename then increment by 1
+skip :: SubstVar v => Env v m n -> Env v m (S n)
+skip e = e .>> shift1E
+
+-- | Shift an environment by size `p`
 upN ::
   forall v p m n.
-  (Subst v v) =>
+  (SubstVar v) =>
   SNat p ->
   Env v m n ->
   Env v (p + m) (p + n)
@@ -137,7 +143,7 @@
     base = MkUpN id
     step :: forall p1. UpN v m n p1 -> UpN v m n (S p1)
     step (MkUpN r) = MkUpN $
-      \e -> var Fin.f0 .: (r e .>> shiftNE s1)
+      \e -> var Fin.f0 .: (skip (r e))
 
 newtype UpN v m n p = MkUpN {getUpN :: Env v m n -> Env v (p + m) (p + n)}
 
diff --git a/src/Rebound/Env/Lazy.hs b/src/Rebound/Env/Lazy.hs
--- a/src/Rebound/Env/Lazy.hs
+++ b/src/Rebound/Env/Lazy.hs
@@ -1,6 +1,6 @@
 {-# LANGUAGE DefaultSignatures #-}
 {-# LANGUAGE UndecidableSuperClasses #-}
-{-# OPTIONS_HADDOCK hide #-}
+-- | The concrete implementation of environments
 module Rebound.Env.Lazy where
 
 -- "Defunctionalized" representation of environment
@@ -115,7 +115,7 @@
 {-# INLINEABLE weakenE' #-}
 
 -- | Shift the term, increasing every free variable as well as the bound by the provided amount.
-shiftNE :: (SubstVar v) => (SubstVar v) => SNat m -> Env v n (m + n)
+shiftNE :: (SubstVar v) => SNat m -> Env v n (m + n)
 shiftNE = Inc
 {-# INLINEABLE shiftNE #-}
 
diff --git a/src/Rebound/Env/ShiftList.hs b/src/Rebound/Env/ShiftList.hs
new file mode 100644
--- /dev/null
+++ b/src/Rebound/Env/ShiftList.hs
@@ -0,0 +1,170 @@
+-- This implementation is adapted from
+-- https://mathisbd.github.io/blog/esubstitutions.html
+-- TODO: still missing weakenER, but should be able to test and run it now
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
+module Rebound.Env.ShiftList where
+
+import Data.Nat
+import Data.Fin
+
+import Rebound.Lib 
+import GHC.Generics hiding (S)
+import Control.DeepSeq (NFData (..))
+
+------------------------------------------------------------------------------
+-- Substitution class declarations
+------------------------------------------------------------------------------
+-- | Well-scoped types that can be the range of
+-- an environment. This should generally be the @Var@
+-- constructor from the syntax.
+class (Subst v v) => SubstVar (v :: Nat -> Type) where
+  var :: Fin n -> v n
+
+
+-- | Apply the environment throughout a term of
+-- type `c n`, replacing variables with values
+-- of type `v m`
+class (SubstVar v) => Subst v c where
+  applyE :: Env v n m -> c n -> c m
+  default applyE :: (Generic1 c, GSubst v (Rep1 c), SubstVar v) => Env v m n -> c m -> c n
+  applyE = gapplyE
+  {-# INLINE applyE #-}
+  isVar :: c n -> Maybe (v :~: c, Fin n)
+  isVar _ = Nothing
+  {-# INLINE isVar #-}
+
+-- | Generic programming variant of 'applyE'.
+gapplyE :: forall c v m n. (Generic1 c, GSubst v (Rep1 c), Subst v c) => Env v m n -> c m -> c n
+gapplyE r e | Just (Refl, x) <- isVar @v @c e = applyEnv r x
+gapplyE r e = applyOpt (\s x -> to1 $ gsubst s (from1 x)) r e
+{-# INLINEABLE gapplyE #-}
+
+-- | Generic programming support for 'Subst'.
+class GSubst v (e :: Nat -> Type) where
+  gsubst :: Env v m n -> e m -> e n
+
+
+------------------------------------------------------------------------------
+-- Environment representation
+------------------------------------------------------------------------------
+
+-- The 'SNat k' in this representation is an embedded shift 
+-- that means that 'Inc k' is the same as 'Inc k'
+data Env a m n where
+    Zero :: Env a Z n
+    Inc  :: !(SNat k) -> Env a n (k + n)
+    Cons :: !(SNat k) -> a m -> (Env a n m) -> Env a (S n) (k + m)
+
+instance (forall n. NFData (a n)) => NFData (Env a n m) where
+  rnf :: (forall (n1 :: Nat). NFData (a n1)) => Env a n m -> ()
+  rnf Zero = ()
+  rnf (Inc x) = rnf x 
+  rnf (Cons x a xs) = rnf x `seq` rnf a `seq` rnf xs 
+
+------------------------------------------------------------------------------
+-- Application
+------------------------------------------------------------------------------
+
+weaken :: forall a k n. Subst a a => SNat k -> a n -> a (k + n)
+weaken k t = applyE @a (shiftNE k) t
+
+applyEnv ::  SubstVar a => Env a n m -> Fin n -> a m
+applyEnv s i = applyRec @N0 snat s i
+{-# INLINEABLE applyEnv #-}
+
+-- | Build an optimized version of applyE.
+-- Checks to see if we are applying the identity substitution first.
+applyOpt :: (Env v n m -> c n -> c m) -> (Env v n m -> c n -> c m)
+applyOpt f (Inc SZ) x = x
+applyOpt f r x = f r x
+{-# INLINEABLE applyOpt #-}
+
+-- | As we traverse the list, accumulate the shifting amount and 
+-- apply it all at once.
+applyRec :: forall acc a n m . SubstVar a => 
+    SNat acc -> Env a n m -> Fin n -> a (acc + m)
+applyRec acc s i = 
+    case s of 
+        Zero -> case i of {}
+        Inc (k :: SNat k) -- renaming
+              | Refl <- axiomPlusZ @m
+              , Refl <- axiomAssoc @acc @k @n
+              -> var (shiftN (sPlus acc k) i)
+        Cons (k :: SNat k) (t :: a m1) s 
+              | Refl <- axiomAssoc @acc @k @m1 
+              -> case i of 
+                   FZ   -> weaken (sPlus acc k) t  -- substitution
+                   FS j -> applyRec (sPlus acc k) s j
+
+
+zeroE :: Env a Z n
+zeroE = Zero
+{-# INLINEABLE zeroE #-}
+
+-- TODO: add weakenER to this definition
+weakenER :: forall m v n. (SubstVar v) => SNat m -> Env v n (n + m)
+weakenER = undefined
+
+shiftNE :: SNat k -> Env a n (k + n)
+shiftNE k = Inc k
+{-# INLINEABLE shiftNE #-}
+
+(.:) :: a m -> Env a n m -> Env a (S n) m
+(.:) = Cons SZ 
+{-# INLINEABLE (.:) #-}
+
+
+-- | inverse of @cons@ -- remove the first mapping
+tail :: (SubstVar v) => Env v (S n) m -> Env v n m
+tail x = shiftNE s1 .>> x
+{-# INLINEABLE tail #-}
+
+-- Compose a substitution with shifting, just add the shifting amount 
+-- to the head of the substitution
+-- skip k s == s .>> Inc k 
+skip0 :: forall k0 a n m. SNatI k0 => Env a n m -> Env a n (k0 + m)
+skip0 s = case s of
+              Zero -> Zero
+              (Inc (k :: SNat k)) 
+                | Refl <- axiomAssoc @k0 @k @n
+                    -> Inc (sPlus (snat @k0) k)
+              (Cons (k :: SNat k) (t :: a m1) s)
+                | Refl <- axiomAssoc @k0 @k @m1
+                    -> Cons (sPlus (snat @k0) k) t s
+{-# INLINEABLE skip0 #-}
+
+up :: forall a n m. SubstVar a => Env a n m -> Env a (S n) (S m)
+up s = var f0 .: (skip0 @N1 s)
+
+-- NB: there is a generic definition of upN in Env.hs, but I don't know 
+-- how efficient it is.
+
+-- | Compose two environments, applying them in sequence (left then right).
+(.>>) :: (SubstVar v) => Env v p n -> Env v n m -> Env v p m
+(.>>) = comp
+{-# INLINEABLE (.>>) #-}
+
+-- | look at the two arguments and compose them together smartly
+comp :: forall a m n p. (SubstVar a) =>
+         Env a m n -> Env a n p -> Env a m p
+comp Zero s = Zero    
+-- if the second argument is a shift, we can use skip    
+comp s (Inc (k :: SNat k)) = withSNat k $ skip0 @k s
+-- if the first argument is a shift, we can drop substitutions in the second
+-- argument
+comp (Inc SZ) s = s
+comp (Inc (snat_ -> SS_ m1)) (Cons (k :: SNat k) _ xs) = 
+    comp (Inc m1) (withSNat k $ skip0 @k xs)
+-- for the Cons/Cons case, we need to apply the second substitution 
+-- to 'x' (after it has been shifted by k)
+comp (Cons (k :: SNat k) (x :: a n1) xs) s = Cons SZ head tail where
+    head = applyE @a (comp (Inc k) s) x
+    tail = comp (withSNat k $ skip0 @k xs) s
+
+-- | Map the range of an environment. Has to preserve the scope of the range.
+transform :: (SubstVar b) => 
+   (forall m. a m -> b m) -> Env a n m -> Env b n m
+transform f Zero = Zero
+transform f (Inc k) = Inc k
+transform f (Cons k x xs) = Cons k (f x) (transform f xs)
diff --git a/src/Rebound/Env/Strict.hs b/src/Rebound/Env/Strict.hs
--- a/src/Rebound/Env/Strict.hs
+++ b/src/Rebound/Env/Strict.hs
@@ -113,7 +113,7 @@
 {-# INLINEABLE weakenE' #-}
 
 -- | increment all free variables by m
-shiftNE :: (SubstVar v) => (SubstVar v) => SNat m -> Env v n (m + n)
+shiftNE :: (SubstVar v) => SNat m -> Env v n (m + n)
 shiftNE = Inc
 {-# INLINEABLE shiftNE #-}
 
diff --git a/src/Rebound/Generics.hs b/src/Rebound/Generics.hs
--- a/src/Rebound/Generics.hs
+++ b/src/Rebound/Generics.hs
@@ -29,6 +29,7 @@
   {-# INLINE gsubst #-}
 
 instance (GSubst b f, GSubst b g) => GSubst b (f :*: g) where
+  gsubst :: (GSubst b f, GSubst b g) => Env b m n -> (:*:) f g m -> (:*:) f g n
   gsubst s (f :*: g) = gsubst s f :*: gsubst s g
   {-# INLINE gsubst #-}
 
@@ -76,7 +77,7 @@
   {-# INLINE gfreeVars #-}
 
 instance (GFV f, GFV g) => GFV (f :*: g) where
-  gappearsFree s (f :*: g) = gappearsFree s f && gappearsFree s g
+  gappearsFree s (f :*: g) = gappearsFree s f || gappearsFree s g
   {-# INLINE gappearsFree #-}
   gfreeVars (f :*: g) = gfreeVars f <> gfreeVars g
   {-# INLINE gfreeVars #-}
diff --git a/test/Examples/DepMatch.hs b/test/Examples/DepMatch.hs
--- a/test/Examples/DepMatch.hs
+++ b/test/Examples/DepMatch.hs
@@ -21,7 +21,6 @@
         ((snat,) <$> patternMatch pat0 tm0) @?= Just (snat @N2, sig Star (Var f0) .: (Star .: zeroE)),
       testCase "Is f0 free in t00?" $ appearsFree f0 t00 @?= True,
       testCase "Is f1 free in t00?" $ appearsFree f1 t00 @?= False,
-      testCase "Weaken t00 by 1" $ weaken' s1 t00 @?= (Var f0 `App` Var f0),
       testCase "Strengthen t00 by 1/1" $ strengthenRec s1 s1 snat t00 @?= Just (Var f0 `App` Var f0),
       testCase "Strengthen t01 by 1/1" $ strengthenRec s1 s1 snat t01 @?= Nothing,
       testCase "Pretty-print t0" $ show t0 @?= "λ_. 0",
diff --git a/test/Examples/PTS.hs b/test/Examples/PTS.hs
--- a/test/Examples/PTS.hs
+++ b/test/Examples/PTS.hs
@@ -22,7 +22,6 @@
     "PTS"
     [ testCase "Is f0 free in t00?" $ appearsFree f0 t00 @?= True,
       testCase "Is f1 free in t00?" $ appearsFree f1 t00 @?= False,
-      testCase "Weaken t00 by 1" $ weaken' s1 t00 @?= App (Var f0) (Var f0),
       testCase "Strengthen t00 by 1/1" $
         strengthenRec s1 s1 snat t00 @?= Just (App (Var f0) (Var f0)),
       testCase "Strengthen t01 by 1/1" $ strengthenRec s1 s1 snat t01 @?= Nothing,