diff --git a/Changelog.md b/Changelog.md
--- a/Changelog.md
+++ b/Changelog.md
@@ -1,3 +1,18 @@
+# 0.1.2
+
+* Added `IsEmbed` typeclass
+
+    * Depend on 'profunctors'
+
+* Changed `embed` and `unembed` to work over any `IsEmbed` type.
+
+* Added `Shift` type for shifting the scope of embedded terms out one level.
+
+# 0.1.1
+
+* Added `isNullDisjointSet` function.
+* Implement a TH `makeClosedAlpha` splice for constructing trivial leaf instances.
+
 # 0.1
 
 * Add `acompare` functiona and `acompare'` method to `Alpha` typeclass.  (christiaanb)
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -18,3 +18,9 @@
 
    You should only notice this if you're implementing an instance of `Alpha` by hand (rather than by using the default
    generic instance).  The original `unbound` returned a `Maybe [AnyName]` here with the same interpretation as `DisjointSet`: `Nothing` means an inconsistency was encountered, or `Just` the free variables of the pattern.
+
+3. `embed :: IsEmbed e => Embedded e -> e` and `unembed :: IsEmbed e => e -> Embedded e`
+
+    The typeclass `IsEmbed` has an `Iso` (again in the sense of the `lens` library) as a method instead of the above pair of methods.
+
+    Again, you should only notice this if you're implementing your own types that are instances of `IsEmbed`.  The easiest thing to do is to use implement `embedded = iso yourEmbed yourUnembed` where `iso` comes from `lens`.  (Although you can also implement it in terms of `dimap` if you don't want to depend on lens)
diff --git a/src/Unbound/Generics/LocallyNameless.hs b/src/Unbound/Generics/LocallyNameless.hs
--- a/src/Unbound/Generics/LocallyNameless.hs
+++ b/src/Unbound/Generics/LocallyNameless.hs
@@ -6,13 +6,22 @@
 -- Stability  : experimental
 --
 --
--- See 'Alpha', 'Bind', "Unbound.Generics.LocallyNameless.Operations" to get started. 
+-- The purpose of @unbound-genrics@ is to simplify the construction of
+-- data structures with rich variable binding structure by providing
+-- generic implementations of alpha-equivalence ('aeq'), free variable
+-- permutation ('swaps'), local and glocal variable freshness
+-- ('lfresh', 'fresh'), 
+--
+--
+-- 
+-- See 'Alpha', 'Bind', "Unbound.Generics.LocallyNameless.Operations" for more information.
 module Unbound.Generics.LocallyNameless (
   module Unbound.Generics.LocallyNameless.Alpha,
   module Unbound.Generics.LocallyNameless.Name,
   module Unbound.Generics.LocallyNameless.Operations,
   module Unbound.Generics.LocallyNameless.Bind,
   module Unbound.Generics.LocallyNameless.Embed,
+  module Unbound.Generics.LocallyNameless.Shift,
   module Unbound.Generics.LocallyNameless.Rebind,
   module Unbound.Generics.LocallyNameless.Rec,
   module Unbound.Generics.LocallyNameless.Fresh,
@@ -24,6 +33,7 @@
 import Unbound.Generics.LocallyNameless.Name hiding (Bn, Fn)
 import Unbound.Generics.LocallyNameless.Bind hiding (B)
 import Unbound.Generics.LocallyNameless.Embed
+import Unbound.Generics.LocallyNameless.Shift
 import Unbound.Generics.LocallyNameless.Rebind hiding (Rebnd)
 import Unbound.Generics.LocallyNameless.Rec
 import Unbound.Generics.LocallyNameless.Fresh
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
@@ -18,6 +18,7 @@
   , inconsistentDisjointSet
   , singletonDisjointSet
   , isConsistentDisjointSet
+  , isNullDisjointSet
   -- * Implementation details
   , NthPatFind
   , NamePatFind
@@ -27,6 +28,8 @@
   , termCtx
   , isTermCtx
   , incrLevelCtx
+  , decrLevelCtx
+  , isZeroLevelCtx
   -- * Internal
   , gaeq
   , gfvAny
@@ -91,6 +94,14 @@
 incrLevelCtx :: AlphaCtx -> AlphaCtx
 incrLevelCtx ctx = ctx { ctxLevel = 1 + ctxLevel ctx }
 
+-- | Decrement the number of binders that we are operating under.
+decrLevelCtx :: AlphaCtx -> AlphaCtx
+decrLevelCtx ctx = ctx { ctxLevel = ctxLevel ctx - 1 }
+
+-- | Are we operating under no binders?
+isZeroLevelCtx :: AlphaCtx -> Bool
+isZeroLevelCtx ctx = ctxLevel ctx == 0
+
 -- | A @DisjointSet a@ is a 'Just' a list of distinct @a@s.  In addition to a monoidal
 -- structure, a disjoint set also has an annihilator 'inconsistentDisjointSet'.
 --
@@ -125,6 +136,11 @@
 isConsistentDisjointSet :: DisjointSet a -> Bool
 isConsistentDisjointSet (DisjointSet Nothing) = False
 isConsistentDisjointSet _ = True
+
+-- | @isNullDisjointSet@ return @True@ iff the given disjoint set is 'mempty'.
+isNullDisjointSet :: DisjointSet a -> Bool
+isNullDisjointSet (DisjointSet (Just [])) = True
+isNullDisjointSet _ = False
 
 -- | Types that are instances of @Alpha@ may participate in name representation.
 --
diff --git a/src/Unbound/Generics/LocallyNameless/Embed.hs b/src/Unbound/Generics/LocallyNameless/Embed.hs
--- a/src/Unbound/Generics/LocallyNameless/Embed.hs
+++ b/src/Unbound/Generics/LocallyNameless/Embed.hs
@@ -7,14 +7,17 @@
 -- Stability  : experimental
 --
 -- The pattern @'Embed' t@ contains a term @t@.
-{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE DeriveGeneric, TypeFamilies #-}
 module Unbound.Generics.LocallyNameless.Embed where
 
 import Control.Applicative (pure, (<$>))
 import Data.Monoid (mempty)
+import Data.Profunctor (Profunctor(..))
+
 import GHC.Generics (Generic)
 
 import Unbound.Generics.LocallyNameless.Alpha
+import Unbound.Generics.LocallyNameless.Internal.Iso (iso)
 
 -- | @Embed@ allows for terms to be /embedded/ within patterns.  Such
 --   embedded terms do not bind names along with the rest of the
@@ -30,6 +33,19 @@
 --   'Shift's at the same time.)
 newtype Embed t = Embed t deriving (Eq, Generic)
 
+class IsEmbed e where
+  type Embedded e :: *
+  -- | Insert or extract the embedded term.
+  -- If you're not using the lens library, see 'Unbound.Generics.LocallyNameless.Operations.embed'
+  -- and 'Unbound.Generics.LocallyNameless.Operations.unembed'
+  -- otherwise 'embedded' is an isomorphism that you can use with lens.
+  -- @embedded :: Iso' (Embedded e) e@
+  embedded :: (Profunctor p, Functor f) => p (Embedded e) (f (Embedded e)) -> p e (f e)
+
+instance IsEmbed (Embed t) where
+  type Embedded (Embed t) = t
+  embedded = iso (\(Embed t) -> t) Embed
+  
 instance Show a => Show (Embed a) where
   showsPrec _ (Embed a) = showString "{" . showsPrec 0 a . showString "}"
 
diff --git a/src/Unbound/Generics/LocallyNameless/Internal/Iso.hs b/src/Unbound/Generics/LocallyNameless/Internal/Iso.hs
new file mode 100644
--- /dev/null
+++ b/src/Unbound/Generics/LocallyNameless/Internal/Iso.hs
@@ -0,0 +1,28 @@
+{-# LANGUAGE RankNTypes #-}
+module Unbound.Generics.LocallyNameless.Internal.Iso where
+
+import Data.Profunctor (Profunctor(..))
+import Data.Functor.Identity (Identity(..))
+
+data Exchange a b s t = Exchange (s -> a) (b -> t)
+
+instance Profunctor (Exchange a b) where
+  dimap f g (Exchange h k) = Exchange (h . f ) (g . k)
+
+type Iso s t a b = forall p f . (Profunctor p, Functor f) => p a (f b) -> p s (f t)
+
+type AnIso s t a b = Exchange a b a (Identity b) -> Exchange a b s (Identity t)
+
+iso :: (s -> a) -> (b -> t) -> Iso s t a b
+iso sa bt = dimap sa (fmap bt)
+{-# INLINE iso #-}
+
+from :: AnIso s t a b -> Iso b a t s
+from l = withIso l $  \ sa bt -> iso bt sa
+{-# INLINE from #-}
+
+withIso :: AnIso s t a b -> ((s -> a) -> (b -> t) -> r) -> r
+withIso ai k =
+  case ai (Exchange id Identity) of
+   Exchange sa bt -> k sa (runIdentity . bt)
+{-# INLINE withIso #-}
diff --git a/src/Unbound/Generics/LocallyNameless/Internal/Lens.hs b/src/Unbound/Generics/LocallyNameless/Internal/Lens.hs
new file mode 100644
--- /dev/null
+++ b/src/Unbound/Generics/LocallyNameless/Internal/Lens.hs
@@ -0,0 +1,11 @@
+module Unbound.Generics.LocallyNameless.Internal.Lens where
+
+import Control.Monad.Reader (MonadReader(..))
+import qualified Control.Monad.Reader as Reader
+import Control.Applicative (Const(..))
+
+type Getting r s a = (a -> Const r a) -> s -> Const r s
+
+view :: MonadReader s m => Getting a s a -> m a
+view l = Reader.asks (getConst . l Const)
+{-# INLINE view #-}
diff --git a/src/Unbound/Generics/LocallyNameless/Operations.hs b/src/Unbound/Generics/LocallyNameless/Operations.hs
--- a/src/Unbound/Generics/LocallyNameless/Operations.hs
+++ b/src/Unbound/Generics/LocallyNameless/Operations.hs
@@ -29,6 +29,7 @@
        , rebind
        , unrebind
        , Embed(..)
+       , IsEmbed(..)
        , embed
        , unembed
          -- * Recursive bindings
@@ -51,10 +52,12 @@
 import Unbound.Generics.LocallyNameless.LFresh
 import Unbound.Generics.LocallyNameless.Name
 import Unbound.Generics.LocallyNameless.Bind
-import Unbound.Generics.LocallyNameless.Embed (Embed(..))
+import Unbound.Generics.LocallyNameless.Embed (Embed(..), IsEmbed(..))
 import Unbound.Generics.LocallyNameless.Rebind
 import Unbound.Generics.LocallyNameless.Rec
 import Unbound.Generics.LocallyNameless.Internal.Fold (toListOf, justFiltered)
+import Unbound.Generics.LocallyNameless.Internal.Lens (view)
+import Unbound.Generics.LocallyNameless.Internal.Iso (from)
 import Unbound.Generics.PermM
 
 -- | @'aeq' t1 t2@ returns @True@ iff @t1@ and @t2@ are alpha-equivalent terms.
@@ -184,13 +187,14 @@
 unrebind :: (Alpha p1, Alpha p2) => Rebind p1 p2 -> (p1, p2)
 unrebind (Rebnd p1 p2) = (p1, open (patternCtx initialCtx) p1 p2)
 
--- | An alias for 'Embed'
-embed :: t -> Embed t
-embed = Embed
+-- | Embeds a term in an 'Embed', or an 'Embed' under some number of 'Shift's
+embed :: IsEmbed e => Embedded e -> e
+embed = view (from embedded)
 
 -- | @'unembed' p@ extracts the term embedded in the pattern @p@.
-unembed :: Embed t -> t
-unembed (Embed t) = t
+-- unembed :: Embed t -> t
+unembed :: IsEmbed e => e -> Embedded e
+unembed = view embedded
 
 -- | Constructor for recursive abstractions.
 trec :: Alpha p => p -> TRec p
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
@@ -7,7 +7,7 @@
 -- Stability  : experimental
 --
 -- The pattern @'Rec' p@ binds the names in @p@ like @p@ itself would,
--- but additinoally, the names in @p@ are scope over @p@.
+-- but additionally, the names in @p@ are scope over @p@.
 --
 -- The term @'TRec' p@ is shorthand for @'Bind' (Rec p) ()@
 {-# LANGUAGE DeriveGeneric #-}
@@ -52,6 +52,9 @@
 instance Alpha p => Alpha (Rec p) where
   isTerm _ = False
   isPat (Rec p) = isPat p
+
+  nthPatFind (Rec p) i = nthPatFind p i
+  namePatFind (Rec p) x = namePatFind p x
 
   open ctx b (Rec p) = Rec (open (incrLevelCtx ctx) b p)
   close ctx b (Rec p) = Rec (close (incrLevelCtx ctx) b p)
diff --git a/src/Unbound/Generics/LocallyNameless/Shift.hs b/src/Unbound/Generics/LocallyNameless/Shift.hs
new file mode 100644
--- /dev/null
+++ b/src/Unbound/Generics/LocallyNameless/Shift.hs
@@ -0,0 +1,93 @@
+{-# OPTIONS_HADDOCK show-extensions #-}
+-- |
+-- Module     : Unbound.Generics.LocallyNameless.Shift
+-- Copyright  : (c) 2015, Aleksey Kliger
+-- License    : BSD3 (See LICENSE)
+-- Maintainer : Aleksey Kliger
+-- Stability  : experimental
+--
+-- The pattern @'Shift' e@ shifts the scope of the embedded term in @e@ one level outwards.
+--
+{-# LANGUAGE TypeFamilies #-}
+module Unbound.Generics.LocallyNameless.Shift where
+
+import Control.Applicative
+import Data.Monoid (Monoid(..))
+
+import Unbound.Generics.LocallyNameless.Alpha (Alpha(..),
+                                               decrLevelCtx, isTermCtx,
+                                               isZeroLevelCtx,
+                                               inconsistentDisjointSet)
+import Unbound.Generics.LocallyNameless.Embed (IsEmbed(..))
+
+import Unbound.Generics.LocallyNameless.Internal.Iso (iso)
+
+-- | The type @Shift e@ is an embedding pattern that shifts the scope of the
+-- free variables of the embedded term @'Embedded' e@ up by one level.
+newtype Shift e = Shift e
+
+instance Functor Shift where
+  fmap f (Shift e) = Shift (f e)
+
+instance IsEmbed e => IsEmbed (Shift e) where
+  type Embedded (Shift e) = Embedded e
+  embedded = iso (\(Shift e) -> e) Shift . embedded
+  
+instance Show e => Show (Shift e) where
+  showsPrec _ (Shift e) = showString "{" . showsPrec 0 e . showString "}"
+
+instance Alpha e => Alpha (Shift e) where
+  isPat (Shift e) = if (isEmbed e) then mempty else inconsistentDisjointSet
+
+  isTerm _ = False
+
+  isEmbed (Shift e) = isEmbed e
+
+  swaps' ctx perm (Shift e) = Shift (swaps' (decrLevelCtx ctx) perm e)
+
+  freshen' ctx p =
+    if isTermCtx ctx
+    then error "LocallyNameless.freshen' called on a term"
+    else return (p, mempty)
+
+  lfreshen' ctx p kont =
+    if isTermCtx ctx
+    then error "LocallyNameless.lfreshen' called on a term"
+    else kont p mempty
+
+  aeq' ctx (Shift e1) (Shift e2) = aeq' ctx e1 e2
+
+  fvAny' ctx afa (Shift e) = Shift <$> fvAny' ctx afa e
+
+  close ctx b se@(Shift e) =
+    if isTermCtx ctx
+    then error "LocallyNameless.close on Shift"
+    else if isZeroLevelCtx ctx
+         then
+           -- consider type A = Rec (Name t, Shift (Embed e), (Embed e))
+           --  (ie the 2nd element of the tuple is not allowed to refer to itself,
+           --   but the third is)
+           -- if we have (x, e1, e2) and we apply 'rec' to it,
+           -- we must close the tuple with respect to itself.
+           -- in that case, the ctxLevel is 0 and so none of the names in
+           -- e1 need be bound.
+           -- on the other hand once we go to
+           --   Bind P (Bind A B) for some P and B,
+           -- the free vars of e1 in A are bound by P.
+           se
+         else Shift (close (decrLevelCtx ctx) b e)
+
+  open ctx b se@(Shift e) =
+    if isTermCtx ctx
+    then error "LocallyNameless.open on Shift"
+    else if isZeroLevelCtx ctx
+         then se
+         else Shift (open (decrLevelCtx ctx) b e)
+
+  nthPatFind (Shift e) i = nthPatFind e i
+  namePatFind (Shift e) x = namePatFind e x
+
+
+  acompare' ctx (Shift x) (Shift y) = acompare' ctx x y
+
+  
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
@@ -55,6 +55,7 @@
 import Unbound.Generics.LocallyNameless.Name
 import Unbound.Generics.LocallyNameless.Alpha
 import Unbound.Generics.LocallyNameless.Embed
+import Unbound.Generics.LocallyNameless.Shift
 import Unbound.Generics.LocallyNameless.Bind
 import Unbound.Generics.LocallyNameless.Rebind
 import Unbound.Generics.LocallyNameless.Rec
@@ -172,6 +173,10 @@
 instance Subst b AnyName where subst _ _ = id ; substs _ = id
 
 instance (Subst c a) => Subst c (Embed a)
+
+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)
 
 instance (Subst c b, Subst c a, Alpha a, Alpha b) => Subst c (Bind a b)
 
diff --git a/src/Unbound/Generics/LocallyNameless/TH.hs b/src/Unbound/Generics/LocallyNameless/TH.hs
new file mode 100644
--- /dev/null
+++ b/src/Unbound/Generics/LocallyNameless/TH.hs
@@ -0,0 +1,68 @@
+{-# OPTIONS_HADDOCK show-extensions #-}
+-- |
+-- Module     : Unbound.Generics.LocallyNameless.TH
+-- Copyright  : (c) 2015, Aleksey Kliger
+-- License    : BSD3 (See LICENSE)
+-- Maintainer : Aleksey Kliger
+-- Stability  : experimental
+--
+-- Template Haskell methods to construct instances of 'Alpha' for
+-- datatypes that don't contain any names and don't participate in
+-- 'Alpha' operations in any non-trivial way.
+{-# LANGUAGE TemplateHaskell #-}
+module Unbound.Generics.LocallyNameless.TH (makeClosedAlpha) where
+import Language.Haskell.TH
+
+import Control.Applicative (Applicative(..))
+import Data.Monoid (Monoid(..))
+import Unbound.Generics.LocallyNameless.Alpha (Alpha(..))
+
+-- | Make a trivial @instance 'Alpha' T@ for a type @T@ that does not
+-- contains no bound nor free values of type @'Name' a@ or @'AnyName'@
+-- (or any in general any values that are themselves non-trivial
+-- instances of 'Alpha').  Use this to write 'Alpha' instances for
+-- types that you don't want to traverse via their @GHC.Generics.Rep@
+-- representation just to find out that there aren't any names.
+--
+-- @@@
+-- data T = T Int deriving (Eq, Ord, Show)
+-- $(makeClosedAlpha T)
+-- -- constructs
+-- -- instance Alpha T where
+-- --   aeq' _ = (==)
+-- --   acompare' _ = compare
+-- --   fvAny' _ _ = pure
+-- --   close _ _ = id
+-- --   open _ _ = id
+-- --   isPat _ = mempty
+-- --   isTerm _ = True
+-- --   nthPatFind _ = Left
+-- --   namePatFind _ _ = Left 0
+-- --   swaps' _ _ = id
+-- --   freshen' _ i = return (i, mempty)
+-- --   lfreshen' _ i cont = cont i mempty
+-- @@@
+--
+makeClosedAlpha :: Name -> DecsQ
+makeClosedAlpha tyName = do
+  
+  let valueD vName e = valD (varP vName) (normalB e) []
+      -- methods :: [Q Dec]
+      methods =
+             [
+               valueD (mkName "aeq'")      [e| \_ctx        -> (==)               |]
+             , valueD (mkName "fvAny'")    [e| \_ctx _nfn   -> pure               |]
+             , valueD 'close               [e| \_ctx _b     -> id                 |]
+             , valueD 'open                [e| \_ctx _b     -> id                 |]
+             , valueD 'isPat               [e| \_           -> mempty             |]
+             , valueD 'isTerm              [e| \_           -> True               |]
+             , valueD 'nthPatFind          [e| \_           -> Left               |]
+             , valueD 'namePatFind         [e| \_ _         -> Left 0             |]
+             , valueD (mkName "swaps'")    [e| \_ctx _p     -> id                 |]
+             , valueD (mkName "freshen'")  [e| \_ctx i      -> return (i, mempty) |]
+             , valueD (mkName "lfreshen'") [e| \_ctx i cont -> cont i mempty      |]
+             , valueD (mkName "acompare'") [e| \_ctx        -> compare            |]
+             ]
+  d <- instanceD (cxt []) (appT [t|Alpha|] (conT tyName)) methods
+  return [d]
+
diff --git a/test/AlphaAssertions.hs b/test/AlphaAssertions.hs
new file mode 100644
--- /dev/null
+++ b/test/AlphaAssertions.hs
@@ -0,0 +1,13 @@
+module AlphaAssertions where
+
+import Test.Tasty.HUnit
+
+import Unbound.Generics.LocallyNameless
+
+assertAeq :: (Alpha t, Show t) => t -> t -> Assertion
+assertAeq x y = assertBool (show x ++ " not alpha equivalent to " ++ show y) (x `aeq` y)
+
+assertAcompare :: (Alpha t, Show t) => t -> t -> Ordering -> Assertion
+assertAcompare x y o =
+  let o' = acompare x y
+  in  assertBool (show x ++ " not alpha-" ++ show o' ++ " to " ++ show y ++ ", but alpha-" ++ show o) (o' == o)
diff --git a/test/Calc.hs b/test/Calc.hs
--- a/test/Calc.hs
+++ b/test/Calc.hs
@@ -14,6 +14,7 @@
 
 import Unbound.Generics.LocallyNameless
 import Unbound.Generics.LocallyNameless.Internal.Fold (toListOf)
+import Unbound.Generics.LocallyNameless.TH
 
 -- variables will range over expressions
 type Var = Name Expr
diff --git a/test/TestACompare.hs b/test/TestACompare.hs
--- a/test/TestACompare.hs
+++ b/test/TestACompare.hs
@@ -8,6 +8,8 @@
 import Test.Tasty
 import Test.Tasty.HUnit
 
+import AlphaAssertions
+
 data Expr
   = V (Name Expr)
   | Add Expr Expr
@@ -15,11 +17,6 @@
   deriving (Show,Generic,Typeable)
 
 instance Alpha Expr
-
-assertAcompare :: (Alpha t, Show t) => t -> t -> Ordering -> Assertion
-assertAcompare x y o =
-  let o' = acompare x y
-  in  assertBool (show x ++ " not alpha-" ++ show o' ++ " to " ++ show y ++ ", but alpha-" ++ show o) (o' == o)
 
 nameA, nameB, nameC :: Name Expr
 nameA = s2n "a"
diff --git a/test/TestCalc.hs b/test/TestCalc.hs
--- a/test/TestCalc.hs
+++ b/test/TestCalc.hs
@@ -14,9 +14,8 @@
 
 import Test.Tasty
 import Test.Tasty.HUnit
-
-assertAeq :: (Alpha t, Show t) => t -> t -> Assertion
-assertAeq x y = assertBool (show x ++ " not alpha equivalent to " ++ show y) (x `aeq` y)
+  
+import AlphaAssertions
 
 test_ex1 :: TestTree
 test_ex1 = testCase "example 1" $ assertAeq (runWhnf emptyEnv ex1) (Just $ C 3)
diff --git a/test/TestShiftEmbed.hs b/test/TestShiftEmbed.hs
new file mode 100644
--- /dev/null
+++ b/test/TestShiftEmbed.hs
@@ -0,0 +1,69 @@
+{-# LANGUAGE DeriveDataTypeable, DeriveGeneric #-}
+module TestShiftEmbed (test_shiftEmbed) where
+
+import Prelude hiding (pi)
+
+import Data.Typeable (Typeable)
+import GHC.Generics (Generic)
+import Unbound.Generics.LocallyNameless
+import qualified Unbound.Generics.PermM as PermM
+
+import AlphaAssertions
+
+import Test.Tasty
+import Test.Tasty.HUnit
+
+type Var = Name Term
+
+data Term
+  = V Var
+  | Pi (Bind (Var, Embed Term) Term)
+  | LetRec (Bind (Rec Decl) Term)
+    deriving (Show, Generic, Typeable)
+
+data Decl =
+  -- a recursive declaration  x : A = m
+  -- where x may occur in m but not in A
+  Decl {
+    declVar :: Var
+    , declClass :: Shift (Embed Term)
+    , declVal :: Embed Term
+    }
+  deriving (Show, Generic, Typeable)
+
+instance Alpha Term
+instance Alpha Decl
+
+x, y, z :: Var
+x = s2n "x"
+y = s2n "y"
+z = s2n "z"
+
+pi :: Var -> Term -> Term -> Term
+pi v a b = Pi $ bind (v, embed a) b
+
+letrec :: Decl -> Term -> Term
+letrec d e = LetRec $ bind (rec d) e
+
+decl :: Var -> Term -> Term -> Decl
+decl v klass e = Decl v (embed klass) (embed e)
+
+
+test_shiftEmbed =
+  testGroup "Embedded and Shifted terms"
+  [
+    testGroup "Embed"
+    [
+      testCase "(pi x:x . x) = (pi y:x . y)" $ let m1 = pi x (V x) (V x)
+                                                   m2 = pi y (V x) (V y)
+                                               in assertAeq m1 m2
+    , testCase "(letrec x : x = x in x) = (letrec y : x = y in y)"
+      $ let m1 = letrec (decl x (V x) (V x)) (V x)
+            m2 = letrec (decl y (V x) (V y)) (V y)
+        in assertAeq m1 m2
+    , testCase "pi x : z . (letrec x : x = x in x) = pi y : z . (letrec x : y = x in x)"
+      $ let m1 = pi x (V z) $ letrec (decl x (V x) (V x)) (V x)
+            m2 = pi y (V z) $ letrec (decl x (V y) (V x)) (V x)
+        in assertAeq m1 m2
+    ]
+  ]
diff --git a/test/TestTH.hs b/test/TestTH.hs
new file mode 100644
--- /dev/null
+++ b/test/TestTH.hs
@@ -0,0 +1,48 @@
+{-# OPTIONS_HADDOCK show-extensions #-}
+-- |
+-- Module     : TestTH
+-- Copyright  : (c) 2015, Aleksey Kliger
+-- License    : BSD3 (See LICENSE)
+-- Maintainer : Aleksey Kliger
+-- Stability  : experimental
+--
+-- Test of 'makeClosedAlpha' splice.
+{-# LANGUAGE TemplateHaskell #-}
+module TestTH (test_TH) where
+
+import Test.Tasty
+import Test.Tasty.HUnit
+import AlphaAssertions
+
+import Unbound.Generics.LocallyNameless
+import Unbound.Generics.LocallyNameless.Internal.Fold (toListOf)
+import Unbound.Generics.LocallyNameless.TH
+
+
+
+data K =
+  KT
+  | KArr K K
+    deriving (Eq, Ord, Show)
+
+$(makeClosedAlpha ''K)
+
+kt, kF, kG :: K
+kt = KT
+kF = KT `KArr` KT
+kG = kF `KArr` KT
+
+emptyPat :: [Name ()]
+emptyPat = []
+
+test_TH :: TestTree
+test_TH = testGroup "TH makeClosedAlpha splice"
+          [ testCase "TH aeq" $ assertAeq kt kt
+          , testCase "TH acompare" $ assertAcompare kt kF (compare kt kF)
+          , testCase "TH fvAny kG" $ assertEqual "" (toListOf fvAny kG) []
+          , testCase "TH close" $ assertEqual "" (close initialCtx emptyPat kt) kt
+          , testCase "TH open" $ assertEqual "" (open initialCtx emptyPat kG) kG
+          , testCase "TH isTerm" $ assertEqual "" (isTerm kF) True
+          , testCase "TH isPat"
+            $ assertBool "isNullDisjointSEt (isPat kF)" (isNullDisjointSet $ isPat kF)
+          ]
diff --git a/test/test-main.hs b/test/test-main.hs
--- a/test/test-main.hs
+++ b/test/test-main.hs
@@ -7,6 +7,8 @@
 import PropOpenClose
 import TinyLam
 import TestACompare
+import TestShiftEmbed
+import TestTH
 
 main :: IO ()
 main = defaultMain $ testGroup "unboundGenerics"
@@ -16,4 +18,6 @@
        , test_openClose
        , test_tinyLam
        , test_acompare
+       , test_shiftEmbed
+       , test_TH
        ]
diff --git a/unbound-generics.cabal b/unbound-generics.cabal
--- a/unbound-generics.cabal
+++ b/unbound-generics.cabal
@@ -2,8 +2,8 @@
 -- documentation, see http://haskell.org/cabal/users-guide/
 
 name:                unbound-generics
-version:             0.1
-synopsis:            Reimplementation of Unbound using GHC Generics
+version:             0.1.2
+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
                      handles the rest!  Automatically derives
@@ -22,7 +22,7 @@
 license-file:        LICENSE
 author:              Aleksey Kliger
 maintainer:          aleksey@lambdageek.org
-copyright:           (c) 2014, Aleksey Kliger
+copyright:           (c) 2014-2015, Aleksey Kliger
 category:            Language
 build-type:          Simple
 extra-source-files:  examples/*.hs,
@@ -39,20 +39,26 @@
                        Unbound.Generics.LocallyNameless.Bind
                        Unbound.Generics.LocallyNameless.Rebind
                        Unbound.Generics.LocallyNameless.Embed
+                       Unbound.Generics.LocallyNameless.Shift
                        Unbound.Generics.LocallyNameless.Operations
                        Unbound.Generics.LocallyNameless.Unsafe
                        Unbound.Generics.LocallyNameless.Internal.Fold
+                       Unbound.Generics.LocallyNameless.Internal.Iso
+                       Unbound.Generics.LocallyNameless.Internal.Lens
                        Unbound.Generics.LocallyNameless.Rec
+                       Unbound.Generics.LocallyNameless.TH
                        Unbound.Generics.PermM
                        Unbound.Generics.LocallyNameless.Subst
   -- other-modules:       
   -- other-extensions:    
   build-depends:       base >=4.6 && <5,
+                       template-haskell >= 2.8.0.0,
                        mtl >= 2.1,
                        transformers >= 0.3,
                        transformers-compat >= 0.3,
                        containers == 0.5.*,
-                       contravariant >= 0.5
+                       contravariant >= 0.5,
+                       profunctors >= 4.0
   hs-source-dirs:      src
   default-language:    Haskell2010
   ghc-options:         -Wall
@@ -60,13 +66,16 @@
 Test-Suite test-unbound-generics
   type:                exitcode-stdio-1.0
   main-is:             test-main.hs
-  other-modules:       Calc
+  other-modules:       AlphaAssertions
+                       Calc
                        TestCalc
                        ParallelReduction
                        TestParallelReduction
                        PropOpenClose
                        TinyLam
                        TestACompare
+                       TestShiftEmbed
+                       TestTH
   build-depends:       base,
                        mtl,
                        tasty,