diff --git a/Data/Binding/Hobbits.hs b/Data/Binding/Hobbits.hs
--- a/Data/Binding/Hobbits.hs
+++ b/Data/Binding/Hobbits.hs
@@ -36,17 +36,20 @@
   module Data.Binding.Hobbits.Liftable,
 
   -- * Ancilliary modules
-  module Data.Type.List,
+  module Data.Proxy, module Data.Type.Equality,
+  module Data.Type.HList,
   -- | Type lists track the types of bound variables.
-  module Data.Binding.Hobbits.NuElim
-  -- | The "Data.Binding.Hobbits.NuElim" module allows elimination of
-  -- bindings and multi-bindings; NOTE: this module is not covered in
-  -- the \"Hobbits for Haskell\" paper.
+  module Data.Binding.Hobbits.NuMatching
+  -- | The "Data.Binding.Hobbits.NuMatching" module exposes the
+  -- | NuMatching class, which allows pattern-matching on (G)ADTs in
+  -- | the bodies of multi-bindings
                             ) where
 
-import Data.Type.List
+import Data.Proxy
+import Data.Type.Equality
+import Data.Type.HList
 import Data.Binding.Hobbits.Mb
 import Data.Binding.Hobbits.Closed
 import Data.Binding.Hobbits.QQ
 import Data.Binding.Hobbits.Liftable
-import Data.Binding.Hobbits.NuElim
+import Data.Binding.Hobbits.NuMatching
diff --git a/Data/Binding/Hobbits/Closed.hs b/Data/Binding/Hobbits/Closed.hs
--- a/Data/Binding/Hobbits/Closed.hs
+++ b/Data/Binding/Hobbits/Closed.hs
@@ -1,8 +1,8 @@
-{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TemplateHaskell, ViewPatterns #-}
 
 -- |
 -- Module      : Data.Binding.Hobbits.Closed
--- Copyright   : (c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul Brauner
+-- Copyright   : (c) 2014 Edwin Westbrook, Nicolas Frisby, and Paul Brauner
 --
 -- License     : BSD3
 --
@@ -18,14 +18,15 @@
   -- * Abstract types
   Cl(),
   -- * Operators involving 'Cl'
-  cl, clApply, unCl, mbApplyCl, mbLiftClosed, noClosedNames,
+  cl, clApply, unCl, noClosedNames,
   -- * Synonyms
   mkClosed, Closed, unClosed
 ) where
 
-import Data.Binding.Hobbits.Internal (Name, Mb(..), Cl(..))
-
-import Data.Binding.Hobbits.NuElim
+import Data.Binding.Hobbits.Internal.Name
+import Data.Binding.Hobbits.Internal.Mb
+import Data.Binding.Hobbits.Internal.Closed
+import Data.Binding.Hobbits.Mb
 
 import Language.Haskell.TH (Q, Exp(..), Type(..))
 import qualified Language.Haskell.TH as TH
@@ -35,9 +36,6 @@
 import qualified Language.Haskell.TH.Syntax as TH
 
 
-
-
-
 -- | @cl@ is used with Template Haskell quotations to create closed terms of
 -- type 'Cl'. A quoted expression is closed if all of the names occuring in it
 -- are
@@ -69,36 +67,27 @@
 
 
 
-
-
 -- | Closed terms are closed (sorry) under application.
 clApply :: Cl (a -> b) -> Cl a -> Cl b
 -- could be defined with cl were it not for the GHC stage restriction
 clApply (Cl f) (Cl a) = Cl (f a)
 
 -- | Closed multi-bindings are also closed under application.
-clMbApply :: (NuElim a, NuElim b) => Cl (Mb ctx (a -> b)) -> Cl (Mb ctx a) ->
+clMbApply :: Cl (Mb ctx (a -> b)) -> Cl (Mb ctx a) ->
              Cl (Mb ctx b)
 clMbApply (Cl f) (Cl a) = Cl (mbApply f a)
 
--- | @mbLiftClosed@ is safe because closed terms don't contain names.
-mbLiftClosed :: Mb ctx (Cl a) -> Cl a
-mbLiftClosed (MkMb _ a) = a
-
 -- | @noClosedNames@ encodes the hobbits guarantee that no name can escape its
 -- multi-binding.
 noClosedNames :: Cl (Name a) -> b
-noClosedNames _ = error $ "... Clever girl!" ++
-  "The `noClosedNames' invariant has somehow been violated."
-
--- | @mbApplyCl@ @f@ @b@ applies a closed function @f@ to the body of
--- multi-binding @b@. For example:
---
--- > mbApplyCl $(cl [| f |]) (nu $ \n -> n)   =   nu f
-mbApplyCl :: Cl (a -> b) -> Mb ctx a -> Mb ctx b
-mbApplyCl f (MkMb names i) = MkMb names (unCl f i)
-
-
+noClosedNames (Cl n) =
+  -- We compare n to itself to force evaluation, in case the body of
+  -- the closed value is non-terminating...
+  case cmpName n n of
+    _ ->
+      error $
+      "... Clever girl!" ++
+      "The `noClosedNames' invariant has somehow been violated."
 
 -- | @mkClosed = cl@
 mkClosed = cl
diff --git a/Data/Binding/Hobbits/Examples/LambdaLifting.hs b/Data/Binding/Hobbits/Examples/LambdaLifting.hs
--- a/Data/Binding/Hobbits/Examples/LambdaLifting.hs
+++ b/Data/Binding/Hobbits/Examples/LambdaLifting.hs
@@ -32,8 +32,7 @@
   ) where
 
 import Data.Binding.Hobbits
-import qualified Data.Type.List.Map as C
-import qualified Data.Type.List.Proof.Member as Mem
+import qualified Data.Type.HList as C
 
 import Data.Binding.Hobbits.Examples.LambdaLifting.Terms
 
@@ -47,7 +46,7 @@
 ------------------------------------------------------------
 
 data LType a where LType :: LType (L a)
-type LC c = MapC LType c
+type LC c = HList LType c
 
 type family AddArrows c b
 type instance AddArrows Nil b = b
@@ -71,13 +70,13 @@
 
 
 boundParams ::
-  lc ~ (lc0 :> b) => LC lc -> (MapC Name lc -> DTerm a) ->
+  lc ~ (lc0 :> b) => LC lc -> (HList Name lc -> DTerm a) ->
                      Decl (AddArrows lc a)
 boundParams (lc0 :> LType) k = -- flagged as non-exhaustive, in spite of type
   freeParams lc0 (\ns -> Decl_One $ nu $ \n -> k (ns :> n))
 
 freeParams ::
-  LC lc -> (MapC Name lc -> Decl a) -> Decl (AddArrows lc a)
+  LC lc -> (HList Name lc -> Decl a) -> Decl (AddArrows lc a)
 freeParams Nil k = k C.empty
 freeParams (lc :> LType) k =
     freeParams lc (\names -> Decl_Cons $ nu $ \x -> k (names :> x))
@@ -87,7 +86,7 @@
 ------------------------------------------------------------
 
 -- FIXME: use this type in place of functions
-type SubC c' c = MapC Name c -> MapC Name c'
+type SubC c' c = HList Name c -> HList Name c'
 
 ------------------------------------------------------------
 -- operations on contexts of free variables
@@ -96,7 +95,7 @@
 data MbLName c a where
     MbLName :: Mb c (Name (L a)) -> MbLName c (L a)
 
-type FVList c fvs = MapC (MbLName c) fvs
+type FVList c fvs = HList (MbLName c) fvs
 
 -- unioning free variable contexts: the data structure
 data FVUnionRet c fvs1 fvs2 where
@@ -109,12 +108,12 @@
   FVUnionRet fvs f1 f2 -> case elemMC fv2 fvs of
     Nothing -> FVUnionRet (fvs :> fv2)
                (\(xs :> _) -> f1 xs) (\(xs :> x) -> f2 xs :> x)
-    Just idx -> FVUnionRet fvs f1 (\xs -> f2 xs :> C.lookup idx xs)
+    Just idx -> FVUnionRet fvs f1 (\xs -> f2 xs :> C.hlistLookup idx xs)
 fvUnion (fvs1 :> fv1) fvs2 = case fvUnion fvs1 fvs2 of
   FVUnionRet fvs f1 f2 -> case elemMC fv1 fvs of
     Nothing -> FVUnionRet (fvs :> fv1)
                (\(xs :> x) -> f1 xs :> x) (\(xs :> _) -> f2 xs)
-    Just idx -> FVUnionRet fvs (\xs -> f1 xs :> C.lookup idx xs) f2
+    Just idx -> FVUnionRet fvs (\xs -> f1 xs :> C.hlistLookup idx xs) f2
 
 elemMC :: MbLName c a -> FVList c fvs -> Maybe (Member fvs a)
 elemMC _ Nil = Nothing
@@ -132,9 +131,9 @@
     SDVar :: Name (D a) -> STerm c a
     SApp :: STerm c (a -> b) -> STerm c a -> STerm c b
 
-skelSubst :: STerm c a -> MapC Name c -> DTerm a
+skelSubst :: STerm c a -> HList Name c -> DTerm a
 skelSubst (SWeaken f db) names = skelSubst db $ f names
-skelSubst (SVar inC) names = TVar $ C.lookup inC names
+skelSubst (SVar inC) names = TVar $ C.hlistLookup inC names
 skelSubst (SDVar dTVar) _ = TDVar dTVar
 skelSubst (SApp db1 db2) names = TApp (skelSubst db1 names) (skelSubst db2 names)
 
@@ -143,7 +142,7 @@
   STerm fvs (AddArrows fvs a) -> FVList c fvs -> STerm fvs a
 skelAppMultiNames db args = skelAppMultiNamesH db args (C.members args) where
   skelAppMultiNamesH ::
-    STerm fvs (AddArrows args a) -> FVList c args -> MapC (Member fvs) args ->
+    STerm fvs (AddArrows args a) -> FVList c args -> HList (Member fvs) args ->
     STerm fvs a
   skelAppMultiNamesH fvs Nil _ = fvs
   -- flagged as non-exhaustive, in spite of type
@@ -158,29 +157,33 @@
     FVSTerm :: FVList c fvs -> STerm (fvs :++: lc) a -> FVSTerm c lc a
 
 fvSSepLTVars ::
-  MapC f lc -> FVSTerm (c :++: lc) Nil a -> FVSTerm c lc a
+  HList f lc -> FVSTerm (c :++: lc) Nil a -> FVSTerm c lc a
 fvSSepLTVars lc (FVSTerm fvs db) = case fvSSepLTVarsH lc Proxy fvs of
   SepRet fvs' f -> FVSTerm fvs' (SWeaken f db)
 
 data SepRet lc c fvs where
   SepRet :: FVList c fvs' -> SubC fvs (fvs' :++: lc) -> SepRet lc c fvs
 
+-- | Create a 'Proxy' object for the type list of a 'HList' vector.
+proxyOfHList :: HList f c -> Proxy c
+proxyOfHList _ = Proxy
+
 fvSSepLTVarsH ::
-  MapC f lc -> Proxy c -> FVList (c :++: lc) fvs -> SepRet lc c fvs
+  HList f lc -> Proxy c -> FVList (c :++: lc) fvs -> SepRet lc c fvs
 fvSSepLTVarsH _ _ Nil = SepRet Nil (\_ -> Nil)
 fvSSepLTVarsH lc c (fvs :> fv@(MbLName n)) = case fvSSepLTVarsH lc c fvs of
   SepRet m f -> case raiseAppName (C.mkMonoAppend c lc) n of
-    Left idx -> SepRet m (\xs -> f xs :> C.lookup (Mem.weakenL (C.proxy m) idx) xs)
+    Left idx -> SepRet m (\xs -> f xs :> C.hlistLookup (C.weakenMemberL (proxyOfHList m) idx) xs)
     Right n -> SepRet (m :> MbLName n)
-               (\xs -> case C.split (C.mkMonoAppend c' lc) xs of
+               (\xs -> case C.splitHList c' lc xs of
                          (fvs' :> fv', lcs) ->
-                           f (C.append fvs' lcs) :> fv')
-    where c' = proxyCons (C.proxy m) fv
+                           f (appendHList fvs' lcs) :> fv')
+    where c' = proxyCons (proxyOfHList m) fv
 
 raiseAppName ::
-  Append c1 c2 c -> Mb c (Name a) -> Either (Member c2 a) (Mb c1 (Name a))
+  Append c1 c2 (c1 :++: c2) -> Mb (c1 :++: c2) (Name a) -> Either (Member c2 a) (Mb c1 (Name a))
 raiseAppName app n =
-  case mbApplyCl $(mkClosed [| mbNameBoundP |]) (mbSeparate app n) of
+  case fmap mbNameBoundP (mbSeparate (proxiesFromAppend app) n) of
     [nuP| Left mem |] -> Left $ mbLift mem
     [nuP| Right n |] -> Right n
 
@@ -200,23 +203,23 @@
   return $ FVSTerm names $ SApp (SWeaken sub1 db1) (SWeaken sub2 db2)
 llBody c [nuP| Lam b |] = do
   PeelRet lc body <- return $ peelLambdas b
-  llret <- llBody (C.append c lc) body
+  llret <- llBody (C.appendHList c lc) body
   FVSTerm fvs db <- return $ fvSSepLTVars lc llret
   cont $ \k ->
     Decls_Cons (freeParams (fvsToLC fvs) $ \names1 ->
                 boundParams lc $ \names2 ->
-                skelSubst db (C.append names1 names2))
+                skelSubst db (C.appendHList names1 names2))
       $ nu $ \d -> k $ FVSTerm fvs (skelAppMultiNames (SDVar d) fvs)
   where
     fvsToLC :: FVList c lc -> LC lc
-    fvsToLC = C.mapC mbLNameToProof where
+    fvsToLC = C.mapHList mbLNameToProof where
       mbLNameToProof :: MbLName c a -> LType a
       mbLNameToProof (MbLName _) = LType
 
 -- the top-level lambda-lifting function
 lambdaLift :: Term a -> Decls a
 lambdaLift t = runCont (llBody Nil (emptyMb t)) $ \(FVSTerm fvs db) ->
-  Decls_Base (skelSubst db (C.mapC (\(MbLName mbn) -> elimEmptyMb mbn) fvs))
+  Decls_Base (skelSubst db (C.mapHList (\(MbLName mbn) -> elimEmptyMb mbn) fvs))
 
 mbLambdaLift :: Mb c (Term a) -> Mb c (Decls a)
-mbLambdaLift = mbApplyCl $(mkClosed [| lambdaLift |])
+mbLambdaLift = fmap lambdaLift
diff --git a/Data/Binding/Hobbits/Examples/LambdaLifting/Terms.hs b/Data/Binding/Hobbits/Examples/LambdaLifting/Terms.hs
--- a/Data/Binding/Hobbits/Examples/LambdaLifting/Terms.hs
+++ b/Data/Binding/Hobbits/Examples/LambdaLifting/Terms.hs
@@ -1,5 +1,5 @@
 {-# LANGUAGE EmptyDataDecls #-}
-{-# LANGUAGE QuasiQuotes, ViewPatterns #-}
+{-# LANGUAGE TemplateHaskell, Rank2Types, QuasiQuotes, ViewPatterns #-}
 {-# LANGUAGE GADTs, KindSignatures #-}
 
 -- |
@@ -20,12 +20,17 @@
   ) where
 
 import Data.Binding.Hobbits
-import qualified Data.Type.List.Map as C
+import qualified Data.Type.HList as C
 
 -- dummy datatypes for distinguishing Decl names from Lam names
 data L a
 data D a
 
+-- to make a function for HList (for pretty)
+newtype StringF x = StringF String
+unStringF (StringF str) = str
+
+
 ------------------------------------------------------------
 -- source terms
 ------------------------------------------------------------
@@ -36,6 +41,8 @@
   Lam :: Binding (L b) (Term a) -> Term (b -> a)
   App :: Term (b -> a) -> Term b -> Term a
 
+$(mkNuMatching [t| forall a . Term a |])
+
 instance Show (Term a) where show = tpretty
 
 -- helps to build terms without explicitly using nu or Var
@@ -45,10 +52,10 @@
 -- pretty print terms
 tpretty :: Term a -> String
 tpretty t = pretty' (emptyMb t) C.empty 0
-  where pretty' :: Mb c (Term a) -> MapC StringF c -> Int -> String
+  where pretty' :: Mb c (Term a) -> HList StringF c -> Int -> String
         pretty' [nuP| Var b |] varnames n =
             case mbNameBoundP b of
-              Left pf  -> unStringF (C.lookup pf varnames)
+              Left pf  -> unStringF (C.hlistLookup pf varnames)
               Right n -> "(free-var " ++ show n ++ ")"
         pretty' [nuP| Lam b |] varnames n =
             let x = "x" ++ show n in
@@ -66,8 +73,6 @@
   TDVar :: Name (D a) -> DTerm a
   TApp :: DTerm (a -> b) -> DTerm a -> DTerm b
 
-instance Show (DTerm a) where show = pretty
-
 -- we use this type for a definiens instead of putting lambdas on the front
 data Decl :: * -> * where
   Decl_One :: Binding (L a) (DTerm b) -> Decl (a -> b)
@@ -78,21 +83,22 @@
   Decls_Base :: DTerm a -> Decls a
   Decls_Cons :: Decl b -> Binding (D b) (Decls a) -> Decls a
 
+$(mkNuMatching [t| forall a . DTerm a |])
+$(mkNuMatching [t| forall a . Decl a |])
+$(mkNuMatching [t| forall a . Decls a |])
+
+instance Show (DTerm a) where show = pretty
 instance Show (Decls a) where show = decls_pretty
 
 ------------------------------------------------------------
 -- pretty printing
 ------------------------------------------------------------
 
--- to make a function for MapC (for pretty)
-newtype StringF x = StringF String
-unStringF (StringF str) = str
-
 -- pretty print terms
 pretty :: DTerm a -> String
 pretty t = mpretty (emptyMb t) C.empty
 
-mpretty :: Mb c (DTerm a) -> MapC StringF c -> String
+mpretty :: Mb c (DTerm a) -> HList StringF c -> String
 mpretty [nuP| TVar b |] varnames =
     mprettyName (mbNameBoundP b) varnames
 mpretty [nuP| TDVar b |] varnames =
@@ -101,7 +107,7 @@
     "(" ++ mpretty b1 varnames
         ++ " " ++ mpretty b2 varnames ++ ")"
 
-mprettyName (Left pf) varnames = unStringF (C.lookup pf varnames)
+mprettyName (Left pf) varnames = unStringF (C.hlistLookup pf varnames)
 mprettyName (Right n) varnames = "(free-var " ++ (show n) ++ ")"
         
 
@@ -110,7 +116,7 @@
 decls_pretty decls =
     "let\n" ++ (mdecls_pretty (emptyMb decls) C.empty 0)
 
-mdecls_pretty :: Mb c (Decls a) -> MapC StringF c -> Int -> String
+mdecls_pretty :: Mb c (Decls a) -> HList StringF c -> Int -> String
 mdecls_pretty [nuP| Decls_Base t |] varnames n =
     "in " ++ (mpretty t varnames)
 mdecls_pretty [nuP| Decls_Cons decl rest |] varnames n =
@@ -118,7 +124,7 @@
     fname ++ " " ++ (mdecl_pretty decl varnames 0) ++ "\n"
     ++ mdecls_pretty (mbCombine rest) (varnames :> (StringF fname)) (n+1)
 
-mdecl_pretty :: Mb c (Decl a) -> MapC StringF c -> Int -> String
+mdecl_pretty :: Mb c (Decl a) -> HList StringF c -> Int -> String
 mdecl_pretty [nuP| Decl_One t|] varnames n =
   let vname = "x" ++ show n in
   vname ++ " = " ++ mpretty (mbCombine t) (varnames :> StringF vname)
diff --git a/Data/Binding/Hobbits/Examples/UnitTests/NuElimTest.hs b/Data/Binding/Hobbits/Examples/UnitTests/NuElimTest.hs
deleted file mode 100644
--- a/Data/Binding/Hobbits/Examples/UnitTests/NuElimTest.hs
+++ /dev/null
@@ -1,49 +0,0 @@
-{-# LANGUAGE GADTs, RankNTypes, TypeOperators, ViewPatterns, TypeFamilies, FlexibleInstances, FlexibleContexts, TemplateHaskell, UndecidableInstances, ScopedTypeVariables, NoMonomorphismRestriction #-}
-
-module NuElimTest where
-
-import Data.Binding.Hobbits
-
-
---
--- some helpers
---
-
-proxies2 = Nil :> Proxy :> Proxy
-
-nu2 :: (Name a1 -> Name a2 -> b) -> Mb (Nil :> a1 :> a2) b
-nu2 f = nuMulti proxies2 $ \(Nil :> n1 :> n2) -> f n1 n2
-
-
---
--- test that mbApply works correctly for names in the argument
---
-
-test1f :: Mb (Nil :> a :> a) (Name a -> Int)
-test1f = nu2 $ \n1 n2 n ->
-         case () of
-           () | Just Refl <- cmpName n n1 -> 1
-           () | Just Refl <- cmpName n n2 -> 2
-           _ -> 3
-
-test1a = test1f `mbApply` (nu2 $ \n1 n2 -> n1) -- body should be 1
-test1b = test1f `mbApply` (nu2 $ \n1 n2 -> n2) -- body should be 2
-test1c = nu (\n -> test1f `mbApply` (nu2 $ \n1 n2 -> n)) -- body should be 3
-
-
-
---
--- test that mbApply works correctly for names in the argument and the
--- return value
---
-
-test2f :: Mb (Nil :> a :> a) (Name a -> Name a)
-test2f = nu2 $ \n1 n2 n ->
-         case () of
-           () | Just Refl <- cmpName n n1 -> n2
-           () | Just Refl <- cmpName n n2 -> n1
-           _ -> n
-
-test2a = test2f `mbApply` (nu2 $ \n1 n2 -> n1) -- should be Nu (n1,n2) n2
-test2b = test2f `mbApply` (nu2 $ \n1 n2 -> n2) -- should be Nu (n1,n2) n1
-test2c = nu (\n -> test2f `mbApply` (nu2 $ \n1 n2 -> n)) -- should be Nu (n) (Nu (n1,n2) n)
diff --git a/Data/Binding/Hobbits/Internal.hs b/Data/Binding/Hobbits/Internal.hs
deleted file mode 100644
--- a/Data/Binding/Hobbits/Internal.hs
+++ /dev/null
@@ -1,116 +0,0 @@
-{-# LANGUAGE GADTs, DeriveDataTypeable #-}
-
--- |
--- Module      : Data.Binding.Hobbits.Internal
--- Copyright   : (c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul Brauner
---
--- License     : BSD3
---
--- Maintainer  : emw4@rice.edu
--- Stability   : experimental
--- Portability : GHC
---
--- This module is internal to the Hobbits library, and should not be used
--- directly.
-
-module Data.Binding.Hobbits.Internal where
-
-import Data.Typeable
-import Data.Type.List
-import Unsafe.Coerce (unsafeCoerce)
-import Data.IORef (IORef, newIORef, readIORef, writeIORef)
-import System.IO.Unsafe (unsafePerformIO)
-
--- | A @Name a@ is a bound name that is associated with type @a@.
-newtype Name a = MkName Int deriving (Typeable, Eq)
-
-{-|
-  An @Mb ctx b@ is a multi-binding that binds exactly one name for each
-  type in @ctx@, where @ctx@ has the form @'Nil' ':>' t1 ':>' ... ':>' tn@.
--}
-data Mb ctx b  = MkMb (MapC Name ctx) b deriving Typeable
-
-{-
-instance Typeable a => Typeable (Mb ctx a) where
-    typeOf (MkMb _ x) = mkTyConApp (mkTyCon "Mb")
-                          [mkTyConApp (mkTyCon "Nil") [], typeOf x]
--}
-
-
-{-|
-  The type @Cl a@ represents a closed term of type @a@,
-  i.e., an expression of type @a@ with no free (Haskell) variables.
-  Since this cannot be checked directly in the Haskell type system,
-  the @Cl@ data type is hidden, and the user can only create
-  closed terms using Template Haskell, through the 'mkClosed'
-  operator.
--}
-newtype Cl a = Cl { unCl :: a }
-
-
-
--- building an arbitrary InCtx proof with a given length
--- (this is used internally in HobbitLib)
-
-data ExMember where ExMember :: Member c a -> ExMember
-
--- creating some Member proof of length i
-memberFromLen :: Int -> ExMember
-memberFromLen 0 = ExMember Member_Base
-memberFromLen n = case memberFromLen (n - 1) of
-  ExMember mem -> ExMember (Member_Step mem)
-
--- unsafely creating a *specific* member proof from length i;
--- this is for when we know the ith element of c must be type a
-unsafeLookupC :: Int -> Member c a
-unsafeLookupC n = case memberFromLen n of
-  ExMember mem -> unsafeCoerce mem
-
-
--- building a proxy for each type in some unknown context
-data ExProxy where ExProxy :: MapC Proxy ctx -> ExProxy
-proxyFromLen :: Int -> ExProxy
-proxyFromLen 0 = ExProxy Nil
-proxyFromLen n = case proxyFromLen (n - 1) of
-                   ExProxy proxy -> ExProxy (proxy :> Proxy)
-
--- unsafely building a proxy for each type in ctx from the length n
--- of ctx; this is only safe when we know the length of ctx = n
-unsafeProxyFromLen :: Int -> MapC Proxy ctx
-unsafeProxyFromLen n = case proxyFromLen n of
-                         ExProxy proxy -> unsafeCoerce proxy
-
--- unsafely convert a list of Ints, used to represent names, to
--- names of certain, given types; note that the first name in the
--- list becomes the last name in the output, with the same reversal
--- used in the Mb representation (see, e.g., mbCombine)
-unsafeNamesFromInts :: [Int] -> MapC Name ctx
-unsafeNamesFromInts [] = unsafeCoerce Nil
-unsafeNamesFromInts (x:xs) =
-    unsafeCoerce $ unsafeNamesFromInts xs :> MkName x
-
--------------------------------------------------------------------------------
--- encapsulated impurity
--------------------------------------------------------------------------------
-
--- README: we *cannot* inline counter, because we want all uses
--- of counter to be the same IORef
-counter :: IORef Int
-{-# NOINLINE counter #-}
-counter = unsafePerformIO (newIORef 0)
-
--- README: fresh_name takes a dummy argument that is used in a dummy
--- way to avoid let-floating its body (and thus getting a fresh name
--- exactly once)
--- README: it *is* ok to inline fresh_name because we don't care in
--- what order fresh names are created
-fresh_name :: a -> Int
-fresh_name a = unsafePerformIO $ do 
-    dummyRef <- newIORef a
-    x <- readIORef counter
-    writeIORef counter (x+1)
-    return x
-
-fresh_names :: MapC Name ctx -> MapC Name ctx
-fresh_names Nil = Nil
-fresh_names (names :> n) = fresh_names names :> MkName (fresh_name n)
diff --git a/Data/Binding/Hobbits/Internal/Closed.hs b/Data/Binding/Hobbits/Internal/Closed.hs
new file mode 100644
--- /dev/null
+++ b/Data/Binding/Hobbits/Internal/Closed.hs
@@ -0,0 +1,28 @@
+{-# LANGUAGE TemplateHaskell, ViewPatterns #-}
+
+-- |
+-- Module      : Data.Binding.Hobbits.Closed
+-- Copyright   : (c) 2014 Edwin Westbrook, Nicolas Frisby, and Paul Brauner
+--
+-- License     : BSD3
+--
+-- Maintainer  : emw4@rice.edu
+-- Stability   : experimental
+-- Portability : GHC
+--
+-- This module defines the type @'Cl' a@ of closed objects of type
+-- @a@. Note that, in order to ensure adequacy of the Hobbits
+-- name-binding approach, this representation is hidden from the user,
+-- and so this file should never be imported directly by the user.
+--
+
+module Data.Binding.Hobbits.Internal.Closed where
+
+{-|
+  The type @Cl a@ represents a closed term of type @a@,
+  i.e., an expression of type @a@ with no free (Haskell) variables.
+  Since this cannot be checked directly in the Haskell type system,
+  the @Cl@ data type is hidden, and the user can only create
+  closed terms using Template Haskell, through the 'cl' operator.
+-}
+newtype Cl a = Cl { unCl :: a }
diff --git a/Data/Binding/Hobbits/Internal/Mb.hs b/Data/Binding/Hobbits/Internal/Mb.hs
new file mode 100644
--- /dev/null
+++ b/Data/Binding/Hobbits/Internal/Mb.hs
@@ -0,0 +1,101 @@
+{-# LANGUAGE GADTs, DeriveDataTypeable, Rank2Types, ViewPatterns #-}
+
+-- |
+-- Module      : Data.Binding.Hobbits.Internal.Name
+-- Copyright   : (c) 2014 Edwin Westbrook, Nicolas Frisby, and Paul Brauner
+--
+-- License     : BSD3
+--
+-- Maintainer  : westbrook@kestrel.edu
+-- Stability   : experimental
+-- Portability : GHC
+--
+-- This module defines the type @'Mb' ctx a@. In order to ensure
+-- adequacy of the Hobbits name-binding approach, this representation
+-- is hidden, and so this file should never be imported directly by
+-- the user.
+--
+
+module Data.Binding.Hobbits.Internal.Mb where
+
+import Data.Typeable
+import Data.Proxy
+import Data.Type.Equality
+import Data.Type.HList
+
+import Data.Binding.Hobbits.Internal.Name
+
+
+{-|
+  An @Mb ctx b@ is a multi-binding that binds one name for each type
+  in @ctx@, where @ctx@ has the form @'Nil' ':>' t1 ':>' ... ':>' tn@.
+  Internally, multi-bindings are represented either as "fresh
+  functions", which are functions that quantify over all fresh names
+  that have not been used before and map them to the body of the
+  binding, or as "fresh pairs", which are pairs of a list of names
+  that are guaranteed to be fresh along with a body. Note that fresh
+  pairs must come with an 'MbTypeRepr' for the body type, to ensure
+  that the names given in the pair can be relaced by fresher names.
+-}
+data Mb ctx b
+    = MkMbFun (HList Proxy ctx) (HList Name ctx -> b)
+    | MkMbPair (MbTypeRepr b) (HList Name ctx) b
+    deriving Typeable
+
+
+{-|
+   This type states that it is possible to replace free names with
+   fresh names in an object of type @a@. This type essentially just
+   captures a representation of the type a as either a Name type, a
+   multi-binding, a function type, or a (G)ADT. In order to be sure
+   that only the "right" proofs are used for (G)ADTs, however, this
+   type is hidden from the user, and can only be constructed with
+   'mkNuMatching'.
+-}
+
+data MbTypeRepr a where
+    MbTypeReprName :: MbTypeRepr (Name a)
+    MbTypeReprMb :: MbTypeRepr a -> MbTypeRepr (Mb ctx a)
+    MbTypeReprFun :: MbTypeRepr a -> MbTypeRepr b -> MbTypeRepr (a -> b)
+    MbTypeReprData :: MbTypeReprData a -> MbTypeRepr a
+
+data MbTypeReprData a =
+    MkMbTypeReprData (forall ctx. HList Name ctx -> HList Name ctx -> a -> a)
+
+
+{-|
+  The call @mapNamesPf data ns ns' a@ replaces each occurrence of a
+  free name in @a@ which is listed in @ns@ by the corresponding name
+  listed in @ns'@. This is similar to the name-swapping of Nominal
+  Logic, except that the swapping does not go both ways.
+-}
+mapNamesPf :: MbTypeRepr a -> HList Name ctx -> HList Name ctx -> a -> a
+mapNamesPf MbTypeReprName Nil Nil n = n
+mapNamesPf MbTypeReprName (names :> m) (names' :> m') n =
+    case cmpName m n of
+      Just Refl -> m'
+      Nothing -> mapNamesPf MbTypeReprName names names' n
+mapNamesPf MbTypeReprName _ _ _ = error "Should not be possible! (in mapNamesPf)"
+mapNamesPf (MbTypeReprMb tRepr) names1 names2 (ensureFreshFun -> (proxies, f)) =
+    -- README: the fresh function created below is *guaranteed* to not
+    -- be passed elements of either names1 or names2, since it should
+    -- only ever be passed fresh names
+    MkMbFun proxies (\ns -> mapNamesPf tRepr names1 names2 (f ns))
+mapNamesPf (MbTypeReprFun tReprIn tReprOut) names names' f =
+    (mapNamesPf tReprOut names names') . f . (mapNamesPf tReprIn names' names)
+mapNamesPf (MbTypeReprData (MkMbTypeReprData mapFun)) names names' x =
+    mapFun names names' x
+
+
+-- | Ensures a multi-binding is in "fresh function" form
+ensureFreshFun :: Mb ctx a -> (HList Proxy ctx, HList Name ctx -> a)
+ensureFreshFun (MkMbFun proxies f) = (proxies, f)
+ensureFreshFun (MkMbPair tRepr ns body) =
+    (mapHList (\_ -> Proxy) ns, \ns' -> mapNamesPf tRepr ns ns' body)
+
+-- | Ensures a multi-binding is in "fresh pair" form
+ensureFreshPair :: Mb ctx a -> (HList Name ctx, a)
+ensureFreshPair (MkMbPair _ ns body) = (ns, body)
+ensureFreshPair (MkMbFun proxies f) =
+    let ns = mapHList (MkName . fresh_name) proxies in
+    (ns, f ns)
diff --git a/Data/Binding/Hobbits/Internal/Name.hs b/Data/Binding/Hobbits/Internal/Name.hs
new file mode 100644
--- /dev/null
+++ b/Data/Binding/Hobbits/Internal/Name.hs
@@ -0,0 +1,134 @@
+{-# LANGUAGE GADTs, DeriveDataTypeable, FlexibleInstances, TypeOperators #-}
+
+-- |
+-- Module      : Data.Binding.Hobbits.Internal.Name
+-- Copyright   : (c) 2014 Edwin Westbrook, Nicolas Frisby, and Paul Brauner
+--
+-- License     : BSD3
+--
+-- Maintainer  : westbrook@kestrel.edu
+-- Stability   : experimental
+-- Portability : GHC
+--
+-- This module defines the type @'Name' a@ as a wrapper around a fresh
+-- integer. Note that, in order to ensure adequacy of the Hobbits
+-- name-binding approach, this representation is hidden from the user,
+-- and so this file should never be imported directly by the user.
+--
+
+module Data.Binding.Hobbits.Internal.Name where
+
+import Data.List
+import Data.Functor.Constant
+import Data.Typeable
+import Data.Type.Equality ((:~:))
+import Unsafe.Coerce (unsafeCoerce)
+import Data.IORef (IORef, newIORef, readIORef, writeIORef)
+import System.IO.Unsafe (unsafePerformIO)
+
+import Data.Type.HList
+
+
+-- | A @Name a@ is a bound name that is associated with type @a@.
+newtype Name a = MkName Int deriving (Typeable, Eq)
+
+instance Show (Name a) where
+  showsPrec _ (MkName n) = showChar '#' . shows n . showChar '#'
+
+instance Show (HList Name c) where
+    show names = "[" ++ (concat $ intersperse "," $ hlistToList $
+                        mapHList (Constant . show) names) ++ "]"
+
+
+-------------------------------------------------------------------------------
+-- Externally visible operators
+-------------------------------------------------------------------------------
+
+{-|
+  @cmpName n m@ compares names @n@ and @m@ of types @Name a@ and @Name b@,
+  respectively. When they are equal, @Some e@ is returned for @e@ a proof
+  of type @a :~: b@ that their types are equal. Otherwise, @None@ is returned.
+
+  For example:
+
+> nu $ \n -> nu $ \m -> cmpName n n   ==   nu $ \n -> nu $ \m -> Some Refl
+> nu $ \n -> nu $ \m -> cmpName n m   ==   nu $ \n -> nu $ \m -> None
+-}
+cmpName :: Name a -> Name b -> Maybe (a :~: b)
+cmpName (MkName n1) (MkName n2)
+  | n1 == n2 = Just $ unsafeCoerce Refl
+  | otherwise = Nothing
+
+
+
+-------------------------------------------------------------------------------
+-- Hidden, unsafe operators
+-------------------------------------------------------------------------------
+
+
+-- building an arbitrary InCtx proof with a given length
+-- (this is used internally in HobbitLib)
+
+data ExMember where ExMember :: Member c a -> ExMember
+
+-- creating some Member proof of length i
+memberFromLen :: Int -> ExMember
+memberFromLen 0 = ExMember Member_Base
+memberFromLen n = case memberFromLen (n - 1) of
+  ExMember mem -> ExMember (Member_Step mem)
+
+-- unsafely creating a *specific* member proof from length i;
+-- this is for when we know the ith element of c must be type a
+unsafeLookupC :: Int -> Member c a
+unsafeLookupC n = case memberFromLen n of
+  ExMember mem -> unsafeCoerce mem
+
+
+-- building a proxy for each type in some unknown context
+data ExProxy where ExProxy :: HList Proxy ctx -> ExProxy
+proxyFromLen :: Int -> ExProxy
+proxyFromLen 0 = ExProxy Nil
+proxyFromLen n = case proxyFromLen (n - 1) of
+                   ExProxy proxy -> ExProxy (proxy :> Proxy)
+
+-- -- unsafely building a proxy for each type in ctx from the length n
+-- -- of ctx; this is only safe when we know the length of ctx = n
+-- unsafeProxyFromLen :: Int -> MapC Proxy ctx
+-- unsafeProxyFromLen n = case proxyFromLen n of
+--                          ExProxy proxy -> unsafeCoerce proxy
+
+-- -- unsafely convert a list of Ints, used to represent names, to
+-- -- names of certain, given types; note that the first name in the
+-- -- list becomes the last name in the output, with the same reversal
+-- -- used in the Mb representation (see, e.g., mbCombine)
+-- unsafeNamesFromInts :: [Int] -> MapC Name ctx
+-- unsafeNamesFromInts [] = unsafeCoerce Nil
+-- unsafeNamesFromInts (x:xs) =
+--     unsafeCoerce $ unsafeNamesFromInts xs :> MkName x
+
+-------------------------------------------------------------------------------
+-- encapsulated impurity
+-------------------------------------------------------------------------------
+
+-- README: we *cannot* inline counter, because we want all uses
+-- of counter to be the same IORef
+counter :: IORef Int
+{-# NOINLINE counter #-}
+counter = unsafePerformIO (newIORef 0)
+
+-- README: fresh_name takes a dummy argument that is used in a dummy
+-- way to avoid let-floating its body (and thus getting a fresh name
+-- exactly once)
+-- README: it *is* ok to inline fresh_name because we don't care in
+-- what order fresh names are created
+fresh_name :: a -> Int
+fresh_name a = unsafePerformIO $ do 
+    dummyRef <- newIORef a
+    x <- readIORef counter
+    writeIORef counter (x+1)
+    return x
+
+-- -- make one fresh name for each name in a given input list
+-- fresh_names :: MapC Name ctx -> MapC Name ctx
+-- fresh_names Nil = Nil
+-- fresh_names (names :> n) = fresh_names names :> MkName (fresh_name n)
diff --git a/Data/Binding/Hobbits/Internal/Utilities.hs b/Data/Binding/Hobbits/Internal/Utilities.hs
new file mode 100644
--- /dev/null
+++ b/Data/Binding/Hobbits/Internal/Utilities.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE Rank2Types #-}
+
+module Data.Binding.Hobbits.Internal.Utilities where
+
+import qualified Data.Generics as SYB
+
+
+
+everywhereButM :: Monad m =>
+  SYB.GenericQ Bool -> SYB.GenericM m -> SYB.GenericM m
+everywhereButM q f x
+  | q x       = return x
+  | otherwise = (SYB.gmapM (everywhereButM q f) x) >>= f
diff --git a/Data/Binding/Hobbits/InternalUtilities.hs b/Data/Binding/Hobbits/InternalUtilities.hs
deleted file mode 100644
--- a/Data/Binding/Hobbits/InternalUtilities.hs
+++ /dev/null
@@ -1,13 +0,0 @@
-{-# LANGUAGE Rank2Types #-}
-
-module Data.Binding.Hobbits.InternalUtilities where
-
-import qualified Data.Generics as SYB
-
-
-
-everywhereButM :: Monad m =>
-  SYB.GenericQ Bool -> SYB.GenericM m -> SYB.GenericM m
-everywhereButM q f x
-  | q x       = return x
-  | otherwise = (SYB.gmapM (everywhereButM q f) x) >>= f
diff --git a/Data/Binding/Hobbits/Liftable.hs b/Data/Binding/Hobbits/Liftable.hs
--- a/Data/Binding/Hobbits/Liftable.hs
+++ b/Data/Binding/Hobbits/Liftable.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE GADTs, TypeOperators, FlexibleInstances, OverlappingInstances, TemplateHaskell, ViewPatterns, QuasiQuotes #-}
+{-# LANGUAGE GADTs, TypeOperators, FlexibleInstances, TemplateHaskell, ViewPatterns, QuasiQuotes #-}
 
 -- |
 -- Module      : Data.Binding.Hobbits.Mb
@@ -18,27 +18,41 @@
 
 module Data.Binding.Hobbits.Liftable where
 
-import Data.Type.List.Proof.Member
-import Data.Binding.Hobbits.Mb
+import Data.Type.HList
+import Data.Binding.Hobbits.Internal.Mb
 import Data.Binding.Hobbits.QQ
+import Data.Binding.Hobbits.Closed
+import Data.Binding.Hobbits.NuMatching
 
 
 {-|
   The class @Liftable a@ gives a \"lifting function\" for a, which can
   take any data of type @a@ out of a multi-binding of type @'Mb' ctx a@.
 -}
-class Liftable a where
+class NuMatching a => Liftable a where
     mbLift :: Mb ctx a -> a
 
+-------------------------------------------------------------------------------
+-- Lifting instances that must be defined inside the library abstraction boundary
+-------------------------------------------------------------------------------
+
+instance Liftable Char where
+    mbLift (ensureFreshPair -> (_, c)) = c
+
 instance Liftable Int where
-    mbLift = mbLiftInt
+    mbLift (ensureFreshPair -> (_, i)) = i
 
 instance Liftable Integer where
-    mbLift = mbLiftInteger
+    mbLift (ensureFreshPair -> (_, i)) = i
 
-instance Liftable Char where
-    mbLift = mbLiftChar
+instance Liftable (Closed a) where
+    mbLift (ensureFreshPair -> (_, c)) = c
 
+
+-------------------------------------------------------------------------------
+-- Lifting instances and related functions that could be defined outside the library
+-------------------------------------------------------------------------------
+
 -- README: this requires overlapping instances, because it clashes
 -- with Liftable2, but this instance is better because it does not
 -- require c nor a to be liftable
@@ -46,6 +60,27 @@
     mbLift [nuP| Member_Base |] = Member_Base
     mbLift [nuP| Member_Step m |] = Member_Step (mbLift m)
 
+-- | Lift a list (but not its elements) out of a multi-binding
+mbList :: NuMatching a => Mb c [a] -> [Mb c a]
+mbList [nuP| [] |] = []
+mbList [nuP| x : xs |] = x : mbList xs
+
+
+-------------------------------------------------------------------------------
+-- Liftable1 and Liftable2
+-------------------------------------------------------------------------------
+
+instance Liftable a => Liftable [a] where
+    mbLift [nuP| [] |] = []
+    mbLift [nuP| x : xs |] = (mbLift x) : (mbLift xs)
+
+instance (Liftable a, Liftable b) => Liftable (a,b) where
+    mbLift [nuP| (x,y) |] = (mbLift x, mbLift y)
+
+-- README: these lead to overlapping instances...
+
+{-
+
 {-|
   The class @Liftable1 f@ gives a lifting function for each type @f a@
   when @a@ itself is @Liftable@.
@@ -73,7 +108,4 @@
 instance (Liftable2 f, Liftable a) => Liftable1 (f a) where
     mbLift1 = mbLift2
 
--- | Lift a list (but not its elements) out of a multi-binding
-mbList :: Mb c [a] -> [Mb c a]
-mbList [nuP| [] |] = []
-mbList [nuP| x : xs |] = x : mbList xs
+-}
diff --git a/Data/Binding/Hobbits/Mb.hs b/Data/Binding/Hobbits/Mb.hs
--- a/Data/Binding/Hobbits/Mb.hs
+++ b/Data/Binding/Hobbits/Mb.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE GADTs, TypeOperators, FlexibleInstances #-}
+{-# LANGUAGE GADTs, TypeOperators, FlexibleInstances, ViewPatterns #-}
 
 -- |
 -- Module      : Data.Binding.Hobbits.Mb
@@ -21,129 +21,66 @@
   Binding(),   -- hides Binding implementation
   Mb(),        -- hides MultiBind implementation
   -- * Multi-binding constructors
-  nu, emptyMb, nuMulti,
-  -- * Operations on multi-bindings
-  elimEmptyMb, mbCombine, mbSeparate, mbToProxy, --mbRearrange,
+  nu, nuMulti, nus, emptyMb,
   -- * Queries on names
-  cmpName, mbCmpName, mbNameBoundP,
-  -- * Special-purpose functions for lifting primitives out of bindings
-  mbLiftChar, mbLiftInt, mbLiftInteger,
-  -- * Synonyms
-  nus
+  cmpName, mbNameBoundP, mbCmpName,
+  -- * Operations on multi-bindings
+  elimEmptyMb, mbCombine, mbSeparate, mbToProxy, mbSwap, mbApply,
+  -- * Eliminators for multi-bindings
+  nuMultiWithElim, nuWithElim, nuMultiWithElim1, nuWithElim1
 ) where
 
-import Data.Type.List
-import Data.Type.List.Map
-import qualified Data.Type.List.Proof.Member as Mem
---import qualified Data.Type.List.Proof.Append as App
-import Data.Binding.Hobbits.Internal
---import qualified Data.Binding.Hobbits.Internal as I
+import Control.Applicative
+import Control.Monad.Identity
 
-import Data.List (intersperse)
-import Data.Functor.Constant
+import Data.Type.Equality ((:~:)(..))
+import Data.Proxy (Proxy(..))
 
 import Unsafe.Coerce (unsafeCoerce)
 
+import Data.Type.HList
+
+import Data.Binding.Hobbits.Internal.Name
+import Data.Binding.Hobbits.Internal.Mb
+--import qualified Data.Binding.Hobbits.Internal as I
+
 -------------------------------------------------------------------------------
--- bindings
+-- creating bindings
 -------------------------------------------------------------------------------
 
 -- | A @Binding@ is simply a multi-binding that binds one name
 type Binding a = Mb (Nil :> a)
 
-instance Show (Name a) where
-  showsPrec _ (MkName n) = showChar '#' . shows n . showChar '#'
-
-instance Show (MapC Name c) where
-    show mapc = "[" ++ (concat $ intersperse "," $ mapCToList $
-                        mapC (Constant . show) mapc) ++ "]"
-
 -- note: we reverse l to show the inner-most bindings last
 instance Show a => Show (Mb c a) where
-  showsPrec p (MkMb names b) = showParen (p > 10) $
+  showsPrec p (ensureFreshPair -> (names, b)) = showParen (p > 10) $
     showChar '#' . shows names . showChar '.' . shows b
 
--- README: we pass f to fresh_name to avoid let-floating the results
--- of fresh_name (which would always give the same name for each nu)
--- README: is *is* ok to do CSE on multiple copies of nu, because
--- the programmer cannot tell if two distinct (non-nested) nus get the
--- same fresh integer, and two nus that look the same to the CSE engine
--- cannot be nested
--- README: it *is* ok to inline nu because we don't care in
--- what order fresh names are created
 {-|
   @nu f@ creates a binding which binds a fresh name @n@ and whose
   body is the result of @f n@.
 -}
 nu :: (Name a -> b) -> Binding a b
-nu f = let n = fresh_name f in n `seq` MkMb (Nil :> MkName n) (f (MkName n))
-
--- README: inner-most bindings come FIRST
--- | Combines a binding inside another binding into a single binding.
-mbCombine :: Mb c1 (Mb c2 b) -> Mb (c1 :++: c2) b
-mbCombine (MkMb l1 (MkMb l2 b)) = MkMb (append l1 l2) b
-
-{-|
-  Separates a binding into two nested bindings. The first argument, of
-  type @'Append' c1 c2 c@, is a \"phantom\" argument to indicate how
-  the context @c@ should be split.
--}
-mbSeparate :: Append c1 c2 c -> Mb c a -> Mb c1 (Mb c2 a)
-mbSeparate app (MkMb l a) = MkMb d (MkMb t a) where
-  (d, t) = split app l
-
--- | Returns a proxy object that enumerates all the types in ctx.
-mbToProxy :: Mb ctx a -> MapC Proxy ctx
-mbToProxy (MkMb l _) = mapC (\_ -> Proxy) l
-
-{- README: this is unsafe, because the two bindings could share names
-{- |
-  Take a multi-binding inside another multi-binding and move the
-  outer binding inside the ineer one.
--}
-mbRearrange :: Mb ctx1 (Mb ctx2 a) -> Mb ctx2 (Mb ctx1 a)
-mbRearrange (MkMb l1 (MkMb l2 a)) = MkMb l2 (MkMb l1 a)
--}
-
--- | Creates an empty binding that binds 0 names.
-emptyMb :: a -> Mb Nil a
-emptyMb t = MkMb Nil t
+nu f = MkMbFun (Nil :> Proxy) (\(Nil :> n) -> f n)
 
 {-|
   The expression @nuMulti p f@ creates a multi-binding of zero or more
   names, one for each element of the vector @p@. The bound names are
   passed the names to @f@, which returns the body of the
-  multi-binding.  The argument @p@, of type @'Mb' f ctx@, acts as a
+  multi-binding.  The argument @p@, of type @'HList' f ctx@, acts as a
   \"phantom\" argument, used to reify the list of types @ctx@ at the
   term level; thus it is unimportant what the type function @f@ is.
 -}
-nuMulti :: MapC f ctx -> (MapC Name ctx -> b) -> Mb ctx b
-nuMulti Nil f = emptyMb $ f Nil
-nuMulti (proxies :> proxy) f =
-    mbCombine $ nuMulti proxies $ \names -> nu $ \n -> f (names :> n)
+nuMulti :: HList f ctx -> (HList Name ctx -> b) -> Mb ctx b
+nuMulti proxies f = MkMbFun (mapHList (const Proxy) proxies) f
 
-{-|
-  Eliminates an empty binding, returning its body. Note that
-  @elimEmptyMb@ is the inverse of @emptyMb@.
--}
-elimEmptyMb :: Mb Nil a -> a
-elimEmptyMb (MkMb Nil t) = t
---elimEmptyMb _ = error "Should not happen! (elimEmptyMb)"
+-- | @nus = nuMulti@
+nus x = nuMulti x
 
-{-|
-  @cmpName n m@ compares names @n@ and @m@ of types @Name a@ and @Name b@,
-  respectively. When they are equal, @Some e@ is returned for @e@ a proof
-  of type @a :=: b@ that their types are equal. Otherwise, @None@ is returned.
 
-  For example:
-
-> nu $ \n -> nu $ \m -> cmpName n n   ==   nu $ \n -> nu $ \m -> Some Refl
-> nu $ \n -> nu $ \m -> cmpName n m   ==   nu $ \n -> nu $ \m -> None
--}
-cmpName :: Name a -> Name b -> Maybe (a :=: b)
-cmpName (MkName n1) (MkName n2)
-  | n1 == n2 = Just $ unsafeCoerce Refl
-  | otherwise = Nothing
+-------------------------------------------------------------------------------
+-- Queries on Names
+-------------------------------------------------------------------------------
 
 {-|
   Checks if a name is bound in a multi-binding, returning @Left mem@
@@ -157,8 +94,8 @@
 > nu $ \n -> mbNameBoundP (nu $ \m -> n)  ==  nu $ \n -> Right n
 -}
 mbNameBoundP :: Mb ctx (Name a) -> Either (Member ctx a) (Name a)
-mbNameBoundP (MkMb names n) = helper names n where
-    helper :: MapC Name c -> Name a -> Either (Member c a) (Name a)
+mbNameBoundP (ensureFreshPair -> (names, n)) = helper names n where
+    helper :: HList Name c -> Name a -> Either (Member c a) (Name a)
     helper Nil n = Right n
     helper (names :> (MkName i)) (MkName j) | i == j = unsafeCoerce $ Left Member_Base
     helper (names :> _) n = case helper names n of
@@ -180,23 +117,176 @@
   @Some Refl@ is returned when the names are equal and @Nothing@ is
   returned when they are not.
 -}
-mbCmpName :: Mb c (Name a) -> Mb c (Name b) -> Maybe (a :=: b)
+mbCmpName :: Mb c (Name a) -> Mb c (Name b) -> Maybe (a :~: b)
 mbCmpName b1 b2 = case (mbNameBoundP b1, mbNameBoundP b2) of
-  (Left mem1, Left mem2) -> Mem.same mem1 mem2
+  (Left mem1, Left mem2) -> membersEq mem1 mem2
   (Right n1, Right n2) -> cmpName n1 n2
   _ -> Nothing
 
--- | Lifts a @Char@ out of a multi-binding
-mbLiftChar :: Mb c Char -> Char
-mbLiftChar (MkMb _ c) = c
 
--- | Lifts an @Int@ out of a multi-binding
-mbLiftInt :: Mb c Int -> Int
-mbLiftInt (MkMb _ c) = c
+-------------------------------------------------------------------------------
+-- Operations on multi-bindings
+-------------------------------------------------------------------------------
 
--- | Lifts an @Integer@ out of a multi-binding
-mbLiftInteger :: Mb c Integer -> Integer
-mbLiftInteger (MkMb _ c) = c
+-- | Creates an empty binding that binds 0 names.
+emptyMb :: a -> Mb Nil a
+emptyMb body = MkMbFun Nil (\_ -> body)
 
--- | @nus = nuMulti@
-nus x = nuMulti x
+{-|
+  Eliminates an empty binding, returning its body. Note that
+  @elimEmptyMb@ is the inverse of @emptyMb@.
+-}
+elimEmptyMb :: Mb Nil a -> a
+elimEmptyMb (ensureFreshPair -> (_, body)) = body
+
+
+-- Extract the proxy objects from an Mb inside of a fresh function
+freshFunctionProxies :: HList Proxy ctx1 -> (HList Name ctx1 -> Mb ctx2 a) ->
+                        HList Proxy ctx2
+freshFunctionProxies proxies1 f =
+    case f (mapHList (const $ MkName 0) proxies1) of
+      MkMbFun proxies2 _ -> proxies2
+      MkMbPair _ ns _ -> mapHList (const Proxy) ns
+
+
+-- README: inner-most bindings come FIRST
+-- | Combines a binding inside another binding into a single binding.
+mbCombine :: Mb c1 (Mb c2 b) -> Mb (c1 :++: c2) b
+mbCombine (MkMbPair tRepr1 l1 (MkMbPair tRepr2 l2 b)) = MkMbPair tRepr2 (appendHList l1 l2) b
+mbCombine (ensureFreshFun -> (proxies1, f1)) =
+    -- README: we pass in Names with integer value 0 here in order to
+    -- get out the proxies for the inner-most bindings; this is "safe"
+    -- because these proxies should never depend on the names
+    -- themselves
+    let proxies2 = freshFunctionProxies proxies1 f1 in
+    MkMbFun
+    (appendHList proxies1 proxies2)
+    (\ns ->
+         let (ns1, ns2) = splitHList Proxy proxies2 ns in
+         let (_, f2) = ensureFreshFun (f1 ns1) in
+         f2 ns2)
+
+
+{-|
+  Separates a binding into two nested bindings. The first argument, of
+  type @'HList' any c2@, is a \"phantom\" argument to indicate how
+  the context @c@ should be split.
+-}
+mbSeparate :: HList any ctx2 -> Mb (ctx1 :++: ctx2) a ->
+              Mb ctx1 (Mb ctx2 a)
+mbSeparate c2 (MkMbPair tRepr ns a) =
+    MkMbPair (MbTypeReprMb tRepr) ns1 (MkMbPair tRepr ns2 a) where
+        (ns1, ns2) = splitHList Proxy c2 ns
+mbSeparate c2 (MkMbFun proxies f) =
+    MkMbFun proxies1 (\ns1 -> MkMbFun proxies2 (\ns2 -> f (appendHList ns1 ns2)))
+        where
+          (proxies1, proxies2) = splitHList Proxy c2 proxies
+
+
+-- | Returns a proxy object that enumerates all the types in ctx.
+mbToProxy :: Mb ctx a -> HList Proxy ctx
+mbToProxy (MkMbFun proxies _) = proxies
+mbToProxy (MkMbPair _ ns _) = mapHList (\_ -> Proxy) ns
+
+
+{-|
+  Take a multi-binding inside another multi-binding and move the
+  outer binding inside the ineer one.
+-}
+mbSwap :: Mb ctx1 (Mb ctx2 a) -> Mb ctx2 (Mb ctx1 a)
+mbSwap (ensureFreshFun -> (proxies1, f1)) =
+    let proxies2 = freshFunctionProxies proxies1 f1 in
+    MkMbFun proxies2
+      (\ns2 ->
+         MkMbFun proxies1
+         (\ns1 ->
+            snd (ensureFreshFun (f1 ns1)) ns2))
+
+{-|
+  Applies a function in a multi-binding to an argument in a
+  multi-binding that binds the same number and types of names.
+-}
+mbApply :: Mb ctx (a -> b) -> Mb ctx a -> Mb ctx b
+mbApply (ensureFreshFun -> (proxies, f_fun)) (ensureFreshFun -> (_, f_arg)) =
+  MkMbFun proxies (\ns -> f_fun ns $ f_arg ns)
+
+
+-------------------------------------------------------------------------------
+-- Functor and Applicative instances
+-------------------------------------------------------------------------------
+
+instance Functor (Mb ctx) where
+    fmap f mbArg =
+        mbApply (nuMulti (mbToProxy mbArg) (\_ -> f)) mbArg
+
+instance TypeCtx ctx => Applicative (Mb ctx) where
+    pure x = nuMulti typeCtxProxies (const x)
+    (<*>) = mbApply
+
+
+-------------------------------------------------------------------------------
+-- Eliminators for multi-bindings
+-------------------------------------------------------------------------------
+
+-- FIXME: add more examples!!
+{-|
+  The expression @nuWithElimMulti args f@ takes a sequence @args@ of
+  zero or more multi-bindings, each of type @Mb ctx ai@ for the same
+  type context @ctx@ of bound names, and a function @f@ and does the
+  following:
+
+  * Creates a multi-binding that binds names @n1,...,nn@, one name for
+    each type in @ctx@;
+
+  * Substitutes the names @n1,...,nn@ for the names bound by each
+    argument in the @args@ sequence, yielding the bodies of the @args@
+    (using the new name @n@); and then
+
+  * Passes the sequence @n1,...,nn@ along with the result of
+    substituting into @args@ to the function @f@, which then returns
+    the value for the newly created binding.
+
+  Note that the types in @args@ must each have a @NuMatching@ instance;
+  this is represented with the @NuMatchingList@ type class.
+
+  Here are some examples:
+
+> (<*>) :: Mb ctx (a -> b) -> Mb ctx a -> Mb ctx b
+> (<*>) f a =
+>     nuWithElimMulti ('Nil' :> f :> a)
+>                     (\_ ('Nil' :> 'Identity' f' :> 'Identity' a') -> f' a')
+-}
+nuMultiWithElim :: TypeCtx ctx =>
+                   (HList Name ctx -> HList Identity args -> b) ->
+                   HList (Mb ctx) args -> Mb ctx b
+nuMultiWithElim f args =
+  MkMbFun typeCtxProxies
+          (\ns -> f ns $ mapHList (\arg -> Identity $ snd (ensureFreshFun arg) ns) args)
+
+
+{-|
+  Similar to 'nuMultiWithElim' but binds only one name.
+-}
+nuWithElim :: (Name a -> HList Identity args -> b) ->
+              HList (Mb (Nil :> a)) args ->
+              Binding a b
+nuWithElim f args =
+    nuMultiWithElim (\(Nil :> n) -> f n) args
+
+
+{-|
+  Similar to 'nuMultiWithElim' but takes only one argument
+-}
+nuMultiWithElim1 :: TypeCtx ctx => (HList Name ctx -> arg -> b) -> Mb ctx arg ->
+                    Mb ctx b
+nuMultiWithElim1 f arg =
+    nuMultiWithElim (\names (Nil :> Identity arg) -> f names arg) (Nil :> arg)
+
+
+{-|
+  Similar to 'nuMultiWithElim' but takes only one argument that binds
+  a single name.
+-}
+nuWithElim1 :: (Name a -> arg -> b) -> Binding a arg -> Binding a b
+nuWithElim1 f arg =
+  nuWithElim (\n (Nil :> Identity arg) -> f n arg) (Nil :> arg)
diff --git a/Data/Binding/Hobbits/NuElim.hs b/Data/Binding/Hobbits/NuElim.hs
deleted file mode 100644
--- a/Data/Binding/Hobbits/NuElim.hs
+++ /dev/null
@@ -1,585 +0,0 @@
-{-# LANGUAGE GADTs, RankNTypes, TypeOperators, ViewPatterns, TypeFamilies, FlexibleInstances, FlexibleContexts, TemplateHaskell, UndecidableInstances, ScopedTypeVariables #-}
-
-{-|
-
-  This module defines the NuElim typeclass, which allows eliminations
-  of (multi-) bindings. The high-level idea is that, when a fresh name
-  is created with 'nu', the fresh name can also be substituted for the
-  bound name in a binding. See the documentation for 'nuWithElim1' and
-  'nuWithElimMulti' for details.
--}
-
-module Data.Binding.Hobbits.NuElim (
-  mbApply, mbMapAndSwap, mbRearrange,
-  nuMultiWithElim, nuWithElim, nuMultiWithElim1, nuWithElim1,
-  NuElim(..), mkNuElimData, NuElimList(..), NuElim1(..),
-  NuElimProof()
-) where
-
---import Data.Data
-import Data.Binding.Hobbits.Internal
---import Data.Binding.Hobbits.Context
-import Data.Binding.Hobbits.Mb
-import Data.Type.List
-import Data.Type.List.Map
-import Language.Haskell.TH hiding (Name)
-import qualified Language.Haskell.TH as TH
---import Unsafe.Coerce (unsafeCoerce)
-import Control.Monad.State
-import Control.Monad.Identity
-
--- "proofs" that type a is an allowed type for nu-elimination; i.e.,
--- that the multi-binding of an Mb ctx a can be eliminated by nuWithElim
-data NuElimProof a where
-    NuElimName :: NuElimProof (Name a)
-    NuElimMb :: NuElimProof a -> NuElimProof (Mb ctx a)
-    NuElimFun :: NuElimProof a -> NuElimProof b -> NuElimProof (a -> b)
-    NuElimData :: NuElimDataProof a -> NuElimProof a
-
-data NuElimDataProof a =
-    NuElimDataProof (forall ctx. MapC Name ctx -> MapC Name ctx -> a -> a)
-
-
--- map the names in one MapC to the corresponding ones in another
-mapNamesPf :: NuElimProof a -> MapC Name ctx -> MapC Name ctx -> a -> a
-mapNamesPf NuElimName Nil Nil n = n
-mapNamesPf NuElimName (names :> m) (names' :> m') n =
-    case cmpName m n of
-      Just Refl -> m'
-      Nothing -> mapNamesPf NuElimName names names' n
-mapNamesPf NuElimName _ _ _ = error "Should not be possible! (in mapNamesPf)"
-mapNamesPf (NuElimMb nuElim) names1 names2 (MkMb ns b) =
-    let names2' = fresh_names ns in
-    MkMb names2' $ mapNamesPf nuElim (names1 `append` ns) (names2 `append` names2') b
-mapNamesPf (NuElimFun nuElimIn nuElimOut) names names' f =
-    (mapNamesPf nuElimOut names names') . f . (mapNamesPf nuElimIn names' names)
-mapNamesPf (NuElimData (NuElimDataProof mapFun)) names names' x =
-    mapFun names names' x
-
-
--- just like mapNamesPf, except use the NuElim class
-mapNames :: NuElim a => MapC Name ctx -> MapC Name ctx -> a -> a
-mapNames = mapNamesPf nuElimProof
-
-
-{-|
-  Instances of the @NuElim a@ class allow the type @a@ to be used with
-  'nuWithElimMulti' and 'nuWithElim1'. The structure of this class is
-  mostly hidden from the user; see 'mkNuElimData' to see how to create
-  instances of the @NuElim@ class.
--}
-class NuElim a where
-    nuElimProof :: NuElimProof a
-
-instance NuElim (Name a) where
-    nuElimProof = NuElimName
-
-instance (NuElim a, NuElim b) => NuElim (a -> b) where
-    nuElimProof = NuElimFun nuElimProof nuElimProof
-
-{-
-instance NuElim a => NuElim (Mb Nil a) where
-    nuElimProof = NuElimMbNil nuElimProof
-
-instance NuElim (Mb ctx a) => NuElim (Mb (ctx :> c) a) where
-    nuElimProof = NuElimMbCons nuElimProof
--}
-
-instance NuElim a => NuElim (Mb ctx a) where
-    nuElimProof = NuElimMb nuElimProof
-
-instance NuElim Int where
-    nuElimProof = NuElimData (NuElimDataProof $ (\c1 c2 -> id))
-
-instance NuElim Char where
-    nuElimProof = NuElimData (NuElimDataProof $ (\c1 c2 -> id))
-
-instance (NuElim a, NuElim b) => NuElim (a,b) where
-    nuElimProof = NuElimData (NuElimDataProof $ (\c1 c2 (a,b) -> (mapNames c1 c2 a, mapNames c1 c2 b)))
-
-instance (NuElim a, NuElim b, NuElim c) => NuElim (a,b,c) where
-    nuElimProof = NuElimData (NuElimDataProof $ (\c1 c2 (a,b,c) -> (mapNames c1 c2 a, mapNames c1 c2 b, mapNames c1 c2 c)))
-
-instance (NuElim a, NuElim b, NuElim c, NuElim d) => NuElim (a,b,c,d) where
-    nuElimProof = NuElimData (NuElimDataProof $ (\c1 c2 (a,b,c,d) -> (mapNames c1 c2 a, mapNames c1 c2 b, mapNames c1 c2 c, mapNames c1 c2 d)))
-
-instance (NuElim a, NuElim b) => NuElim (Either a b) where
-    nuElimProof = NuElimData
-                  (NuElimDataProof
-                   $ (\c1 c2 x -> case x of
-                                    Left l -> Left (mapNames c1 c2 l)
-                                    Right r -> Right (mapNames c1 c2 r)))
-
-instance NuElim a => NuElim [a] where
-    nuElimProof = NuElimData (NuElimDataProof $ (\c1 c2 -> map (mapNames c1 c2)))
-
-
-{-
-type family NuElimListProof args
-type instance NuElimListProof Nil = ()
-type instance NuElimListProof (args :> arg) = (NuElimListProof args, NuElimProof arg)
-
--- the NuElimList class, for saying that NuElim holds for a context of types
-class NuElimList args where
-    nuElimListProof :: NuElimListProof args
-
-instance NuElimList Nil where
-    nuElimListProof = ()
-
-instance (NuElimList args, NuElim a) => NuElimList (args :> a) where
-    nuElimListProof = (nuElimListProof, nuElimProof)
--}
-
-data NuElimObj a = NuElim a => NuElimObj ()
-
--- the NuElimList class, for saying that NuElim holds for a context of types
-class NuElimList args where
-    nuElimListProof :: MapC NuElimObj args
-
-instance NuElimList Nil where
-    nuElimListProof = Nil
-
-instance (NuElimList args, NuElim a) => NuElimList (args :> a) where
-    nuElimListProof = nuElimListProof :> NuElimObj ()
-
-
-class NuElim1 f where
-    nuElimProof1 :: NuElim a => NuElimObj (f a)
-
--- README: deriving NuElim from NuElim1 leads to overlapping instances
--- for, e.g., Name a
-{-
-instance (NuElim1 f, NuElim a) => NuElim (f a) where
-    nuElimProof = nuElimProof1 nuElimProof
--}
-
-instance (NuElim1 f, NuElimList ctx) => NuElim (MapC f ctx) where
-    nuElimProof = NuElimData $ NuElimDataProof $ helper nuElimListProof where
-        helper :: NuElim1 f =>
-                  MapC NuElimObj args -> MapC Name ctx1 -> MapC Name ctx1 ->
-                  MapC f args -> MapC f args
-        helper Nil c1 c2 Nil = Nil
-        helper (proofs :> NuElimObj ()) c1 c2 (elems :> (elem :: f a)) =
-            case nuElimProof1 :: NuElimObj (f a) of
-              NuElimObj () ->
-                  (helper proofs c1 c2 elems) :>
-                  mapNames c1 c2 elem
-
--- filter out names from a MapC Name
-{-
-data FilterRes where
-    FilterRes :: (MapC Name ctx, MapC Name ctx) -> FilterRes
-
-filterName :: Name a -> MapC Name ctx -> MapC Name ctx -> FilterRes
-filterName n Nil Nil = Nil
-filterName 
-
-filterNames :: [Int] -> MapC Name ctx -> MapC Name ctx -> FilterRes
-filterNames Nil names1 names2 = FilterRes names1 names2
-Nil Nil = FilterRes Nil
-filterNames (names1 :> n1)
--}
-
-{-|
-  Applies a function in a multi-binding to an argument in a
-  multi-binding that binds the same number and types of names.
--}
-mbApply :: (NuElim a, NuElim b) => Mb ctx (a -> b) -> Mb ctx a -> Mb ctx b
-mbApply (MkMb names f) (MkMb names' a) =
-    let names'' = fresh_names names in
-    MkMb names'' $ (mapNames names names'' f) (mapNames names' names'' a)
-
-mbMapAndSwap :: NuElim a => (Mb ctx1 a -> b) -> Mb ctx1 (Mb ctx2 a) -> Mb ctx2 b
-mbMapAndSwap = undefined
-{-
-mbMapAndSwap (MkMb names f) (MkMb names' a) =
-    MkMb names $ f $ mapNames names' names a
--}
-
-{-|
-  Take a multi-binding inside another multi-binding and move the
-  outer binding inside the inner one.
-
-  NOTE: This is not yet implemented.
--}
-mbRearrange :: NuElim a => Mb ctx1 (Mb ctx2 a) -> Mb ctx2 (Mb ctx1 a)
-mbRearrange = mbMapAndSwap id
-
-
-
--- FIXME: add more examples!!
-{-|
-  The expression @nuWithElimMulti args f@ takes a sequence @args@ of
-  zero or more multi-bindings, each of type @Mb ctx ai@ for the same
-  type context @ctx@ of bound names, and a function @f@ and does the
-  following:
-
-  * Creates a multi-binding that binds names @n1,...,nn@, one name for
-    each type in @ctx@;
-
-  * Substitutes the names @n1,...,nn@ for the names bound by each
-    argument in the @args@ sequence, yielding the bodies of the @args@
-    (using the new name @n@); and then
-
-  * Passes the sequence @n1,...,nn@ along with the result of
-    substituting into @args@ to the function @f@, which then returns
-    the value for the newly created binding.
-
-  Note that the types in @args@ must each have a @NuElim@ instance;
-  this is represented with the @NuElimList@ type class.
-
-  Here are some examples:
-
-> commuteFun :: (NuElim a, NuElim b) => Mb ctx (a -> b) -> Mb ctx a -> Mb ctx b
-> commuteFun f a =
->     nuWithElimMulti ('mbToProxy' f) ('Nil' :> f :> a)
->                     (\_ ('Nil' :> 'Identity' f' :> 'Identity' a') -> f' a')
--}
-nuMultiWithElim :: (NuElimList args, NuElim b) =>
-                   MapC f ctx -> MapC (Mb ctx) args ->
-                   (MapC Name ctx -> MapC Identity args -> b) -> Mb ctx b
-nuMultiWithElim nameProxies args f =
-    mbMultiApply (nuMulti nameProxies
-                  (\names -> (mapCToAddArrows args (f names)))) args nuElimListProof where
-        mapCToAddArrows :: MapC f args -> (MapC Identity args -> b) ->
-                           AddArrows args b
-        mapCToAddArrows Nil f = f Nil
-        mapCToAddArrows (args :> _) f = mapCToAddArrows args (\args' x -> f (args' :> Identity x))
-        mbMultiApply :: NuElim b => Mb ctx (AddArrows args b) ->
-                        MapC (Mb ctx) args -> MapC NuElimObj args -> Mb ctx b
-        mbMultiApply mbF Nil Nil = mbF
-        mbMultiApply mbF (args :> arg) (proofs :> NuElimObj ()) =
-            mbApply (mbMultiApply mbF args proofs) arg
-
-
-type family AddArrows ctx a
-type instance AddArrows Nil a = a
-type instance AddArrows (ctx :> b) a = AddArrows ctx (b -> a)
-
--- README: old implementation
-{-
-nuMultiWithElim nameProxies args f =
-    nuMulti nameProxies $ \names -> f names (mapArgs nuElimListProof args names)
-    where
-      mapArgs :: MapC NuElimProof args -> MapC (Mb ctx) args ->
-                 MapC Name ctx -> MapC Identity args
-      mapArgs Nil Nil _ = Nil
-      mapArgs (proofs :> proof) (args :> arg) names =
-          mapArgs proofs args names :>
-                      (Identity $ mapNamesSubst proof names arg)
-      mapArgs _ _ _ = error "Should not be possible! (in mapArgs)"
-
-      mapNamesSubst :: NuElimProof arg -> MapC Name ctx -> Mb ctx arg -> arg
-      mapNamesSubst proof names (MkMb namesOld arg) =
-          mapNamesPf proof namesOld names arg
--}
-
-{-|
-  Similar to 'nuMultiWithElim' but binds only one name.
--}
-nuWithElim :: (NuElimList args, NuElim b) => MapC (Mb (Nil :> a)) args ->
-              (Name a -> MapC Identity args -> b) -> Binding a b
-nuWithElim args f =
-    nuMultiWithElim (Nil :> Proxy) args (\(Nil :> n) -> f n)
-
-
-{-|
-  Similar to 'nuMultiWithElim' but takes only one argument
--}
-nuMultiWithElim1 :: (NuElim arg, NuElim b) => MapC f ctx -> Mb ctx arg ->
-                    (MapC Name ctx -> arg -> b) -> Mb ctx b
-nuMultiWithElim1 nameProxies arg f =
-    nuMultiWithElim nameProxies (Nil :> arg)
-                    (\names (Nil :> Identity arg) -> f names arg)
-
-
-{-|
-  Similar to 'nuMultiWithElim' but takes only one argument that binds
-  a single name.
--}
-nuWithElim1 :: (NuElim arg, NuElim b) => Binding a arg ->
-               (Name a -> arg -> b) -> Binding a b
-nuWithElim1 (MkMb namesOld arg) f =
-    nu $ \n -> f n (mapNames namesOld (Nil :> n) arg)
-{-
-nuWithElim1 (MkMb _ arg) f =
-    error "Internal error in nuWithElim1"
--}
-
-
--- now we define some TH to create NuElimDataProofs
-
-natsFrom i = i : natsFrom (i+1)
-
-fst3 :: (a,b,c) -> a
-fst3 (x,_,_) = x
-
-snd3 :: (a,b,c) -> b
-snd3 (_,y,_) = y
-
-thd3 :: (a,b,c) -> c
-thd3 (_,_,z) = z
-
-
-type Names = (TH.Name, TH.Name, TH.Name, TH.Name)
-
-mapNamesType a = [t| forall ctx. MapC Name ctx -> MapC Name ctx -> $a -> $a |]
-
-{-|
-  Template Haskell function for creating NuElim instances for (G)ADTs.
-  Typical usage is to include the following line in the source file for
-  (G)ADT @T@ (here assumed to have two type arguments):
-
-> $(mkNuElimData [t| forall a b . T a b |])
-
-  The 'mkNuElimData' call here will create an instance declaration for
-  @'NuElim' (T a b)@. It is also possible to include a context in the
-  forall type; for example, if we define the 'ID' data type as follows:
-
-> data ID a = ID a
-
-  then we can create a 'NuElim' instance for it like this:
-
-> $( mkNuElimData [t| NuElim a => ID a |])
-
-  Note that, when a context is included, the Haskell parser will add
-  the @forall a@ for you.
--}
-mkNuElimData :: Q Type -> Q [Dec]
-mkNuElimData tQ =
-    do t <- tQ
-       (cxt, cType, tName, constrs, tyvars) <- getNuElimInfoTop t
-       fName <- newName "f"
-       x1Name <- newName "x1"
-       x2Name <- newName "x2"
-       clauses <- mapM (getClause (tName, fName, x1Name, x2Name)) constrs
-       mapNamesT <- mapNamesType (return cType)
-       return [InstanceD
-               cxt (AppT (ConT ''NuElim) cType)
-               [ValD (VarP 'nuElimProof)
-                (NormalB
-                 $ AppE (ConE 'NuElimData)
-                   $ AppE (ConE 'NuElimDataProof)
-                         $ LetE [SigD fName
-                                 $ ForallT (map PlainTV tyvars) cxt mapNamesT,
-                                 FunD fName clauses]
-                               (VarE fName)) []]]
-
-       {-
-       return (LetE
-               [SigD fName
-                     (ForallT tyvars reqCxt
-                     $ foldl AppT ArrowT
-                           [foldl AppT (ConT conName)
-                                      (map tyVarToType tyvars)]),
-                FunD fname clauses]
-               (VarE fname))
-        -}
-    where
-      -- extract the name from a TyVarBndr
-      tyBndrToName (PlainTV n) = n
-      tyBndrToName (KindedTV n _) = n
-
-      -- fail for getNuElimInfo
-      getNuElimInfoFail t extraMsg =
-          fail ("mkNuElimData: " ++ show t
-                ++ " is not a type constructor for a (G)ADT applied to zero or more distinct type variables" ++ extraMsg)
-
-      -- get info for conName (top-level call)
-      getNuElimInfoTop t = getNuElimInfo [] [] t t
-
-      -- get info for conName
-      getNuElimInfo ctx tyvars topT (ConT tName) =
-          do info <- reify tName
-             case info of
-               TyConI (DataD _ _ tyvarsReq constrs _) ->
-                   success tyvarsReq constrs
-               TyConI (NewtypeD _ _ tyvarsReq constr _) ->
-                   success tyvarsReq [constr]
-               _ -> getNuElimInfoFail topT (": info for " ++ (show tName) ++ " = " ++ (show info))
-          where
-            success tyvarsReq constrs =
-                let tyvarsRet = if tyvars == [] && ctx == []
-                                then map tyBndrToName tyvarsReq
-                                else tyvars in
-                return (ctx,
-                        foldl AppT (ConT tName) (map VarT tyvars),
-                        tName, constrs, tyvarsRet)
-
-      getNuElimInfo ctx tyvars topT (AppT f (VarT argName)) =
-          if elem argName tyvars then
-              getNuElimInfoFail topT ""
-          else
-              getNuElimInfo ctx (argName:tyvars) topT f
-
-      getNuElimInfo ctx tyvars topT (ForallT _ ctx' t) =
-          getNuElimInfo (ctx ++ ctx') tyvars topT t
-
-      getNuElimInfo ctx tyvars topT t = getNuElimInfoFail topT ""
-
-      -- get the name from a data type
-      getTCtor t = getTCtorHelper t t []
-      getTCtorHelper (ConT tName) topT tyvars = Just (topT, tName, tyvars)
-      getTCtorHelper (AppT t1 (VarT var)) topT tyvars =
-          getTCtorHelper t1 topT (tyvars ++ [var])
-      getTCtorHelper (SigT t1 _) topT tyvars = getTCtorHelper t1 topT tyvars
-      getTCtorHelper _ _ _ = Nothing
-
-      -- get a list of Clauses, one for each constructor in constrs
-      getClauses :: Names -> [Con] -> Q [Clause]
-      getClauses names constrs = mapM (getClause names) constrs
-
-      getClause :: Names -> Con -> Q Clause
-      getClause names (NormalC cName cTypes) =
-          getClauseHelper names (map snd cTypes)
-                          (natsFrom 0)
-                          (\l -> ConP cName (map (VarP . fst3) l))
-                          (\l -> foldl AppE (ConE cName) (map fst3 l))
-
-      getClause names (RecC cName cVarTypes) =
-          getClauseHelper names (map thd3 cVarTypes)
-                         (map fst3 cVarTypes)
-                         (\l -> RecP cName
-                                (map (\(var,_,field) -> (field, VarP var)) l))
-                         (\l -> RecConE cName
-                                (map (\(exp,_,field) -> (field, exp)) l))
-
-      getClause names (InfixC cType1 cName cType2) =
-          undefined -- FIXME
-
-      getClause names (ForallC _ _ con) =  getClause names con
-
-      getClauseHelper :: Names -> [Type] -> [a] ->
-                         ([(TH.Name,Type,a)] -> Pat) ->
-                         ([(Exp,Type,a)] -> Exp) ->
-                         Q Clause
-      getClauseHelper names@(tName, fName, x1Name, x2Name) cTypes cData pFun eFun =
-          do varNames <- mapM (newName . ("x" ++) . show . fst)
-                         $ zip (natsFrom 0) cTypes
-             let varsTypesData = zip3 varNames cTypes cData
-             let expsTypesData = map (mkExpTypeData names) varsTypesData
-             return $ Clause [(VarP x1Name), (VarP x2Name), (pFun varsTypesData)]
-                        (NormalB $ eFun expsTypesData) []
-
-      mkExpTypeData :: Names -> (TH.Name,Type,a) -> (Exp,Type,a)
-      mkExpTypeData (tName, fName, x1Name, x2Name)
-                    (varName, getTCtor -> Just (t, tName', _), cData)
-          | tName == tName' =
-              -- the type of the arg is the same as the (G)ADT we are
-              -- recursing over; apply the recursive function
-              (foldl AppE (VarE fName)
-                         [(VarE x1Name), (VarE x2Name), (VarE varName)],
-               t, cData)
-      mkExpTypeData (tName, fName, x1Name, x2Name) (varName, t, cData) =
-          -- the type of the arg is not the same as the (G)ADT; call mapNames
-          (foldl AppE (VarE 'mapNames)
-                     [(VarE x1Name), (VarE x2Name), (VarE varName)],
-           t, cData)
-
--- FIXME: old stuff below
-
-type CxtStateQ a = StateT Cxt Q a
-
--- create a NuElimDataProof for a (G)ADT
-mkNuElimDataProofOld :: Q TH.Name -> Q Exp
-mkNuElimDataProofOld conNameQ =
-    do conName <- conNameQ
-       (cxt, name, tyvars, constrs) <- getNuElimInfo conName
-       (clauses, reqCxt) <- runStateT (getClauses cxt name tyvars constrs) []
-       fname <- newName "f"
-       return (LetE
-               [SigD fname
-                     (ForallT tyvars reqCxt
-                     $ foldl AppT ArrowT
-                           [foldl AppT (ConT conName)
-                                      (map tyVarToType tyvars)]),
-                FunD fname clauses]
-               (VarE fname))
-    where
-      -- convert a TyVar to a Name
-      tyVarToType (PlainTV n) = VarT n
-      tyVarToType (KindedTV n _) = VarT n
-
-      -- get info for conName
-      getNuElimInfo conName =
-          reify conName >>= \info ->
-              case info of
-                TyConI (DataD cxt name tyvars constrs _) ->
-                    return (cxt, name, tyvars, constrs)
-                _ -> fail ("mkNuElimDataProof: " ++ show conName
-                           ++ " is not a (G)ADT")
-      {-
-      -- report failure
-      getNuElimInfoFail t =
-          fail ("mkNuElimDataProof: " ++ show t
-                ++ " is not a fully applied (G)ADT")
-
-      getNuElimInfo (ConT conName) topT =
-          reify conName >>= \info ->
-              case info of
-                TyConI (DataD cxt name tyvars constrs _) ->
-                    return (cxt, name, tyvars, constrs)
-                _ -> getNuElimInfoFail topT
-      getNuElimInfo (AppT t _) topT = getNuElimInfo t topT
-      getNuElimInfo (SigT t _) topT = getNuElimInfo t topT
-      getNuElimInfo _ topT = getNuElimInfoFail topT
-       -}
-
-      -- get a list of Clauses, one for each constructor in constrs
-      getClauses :: Cxt -> TH.Name -> [TyVarBndr] -> [Con] -> CxtStateQ [Clause]
-      getClauses cxt name tyvars constrs =
-          mapM (getClause cxt name tyvars []) constrs
-
-      getClause :: Cxt -> TH.Name -> [TyVarBndr] -> [TyVarBndr] -> Con ->
-                   CxtStateQ Clause
-      getClause cxt name tyvars locTyvars (NormalC cName cTypes) =
-          getClauseHelper cxt name tyvars locTyvars (map snd cTypes)
-                          (natsFrom 0)
-                          (\l -> ConP cName (map (VarP . fst3) l))
-                          (\l -> foldl AppE (ConE cName) (map (VarE . fst3) l))
-
-      getClause cxt name tyvars locTyvars (RecC cName cVarTypes) =
-          getClauseHelper cxt name tyvars locTyvars (map thd3 cVarTypes)
-                         (map fst3 cVarTypes)
-                         (\l -> RecP cName
-                                (map (\(var,_,field) -> (field, VarP var)) l))
-                         (\l -> RecConE cName
-                                (map (\(var,_,field) -> (field, VarE var)) l))
-
-      getClause cxt name tyvars locTyvars (InfixC cType1 cName cType2) =
-          undefined -- FIXME
-
-      getClause cxt name tyvars locTyvars (ForallC tyvars2 cxt2 con) =
-          getClause (cxt ++ cxt2) name tyvars (locTyvars ++ tyvars2) con
-
-      getClauseHelper :: Cxt -> TH.Name -> [TyVarBndr] -> [TyVarBndr] ->
-                         [Type] -> [a] ->
-                         ([(TH.Name,Type,a)] -> Pat) ->
-                         ([(TH.Name,Type,a)] -> Exp) ->
-                         CxtStateQ Clause
-      getClauseHelper cxt name tyvars locTyvars cTypes cData pFun eFun =
-          do varNames <- mapM (lift . newName . ("x" ++) . show . fst)
-                         $ zip (natsFrom 0) cTypes
-             () <- ensureCxt cxt locTyvars cTypes
-             let varsTypesData = zip3 varNames cTypes cData
-             return $ Clause [(pFun varsTypesData)]
-                        (NormalB $ eFun varsTypesData) []
-
-      -- ensure that NuElim a holds for each type a in cTypes
-      ensureCxt :: Cxt -> [TyVarBndr] -> [Type] -> CxtStateQ ()
-      ensureCxt cxt locTyvars cTypes =
-          foldM (const (ensureCxt1 cxt locTyvars)) () cTypes
-
-      -- FIXME: it is not possible (or, at least, not easy) to determine
-      -- if NuElim a is implied from a current Cxt... so we just add
-      -- everything we need to the returned Cxt, except for 
-      ensureCxt1 :: Cxt -> [TyVarBndr] -> Type -> CxtStateQ ()
-      ensureCxt1 cxt locTyvars t = undefined
-      {-
-      ensureCxt1 cxt locTyvars t = do
-        curCxt = get
-        let fullCxt = cxt ++ curCxt
-        isOk <- isNuElim fullCxt 
-
-      isNuElim 
-       -}
diff --git a/Data/Binding/Hobbits/NuMatching.hs b/Data/Binding/Hobbits/NuMatching.hs
new file mode 100644
--- /dev/null
+++ b/Data/Binding/Hobbits/NuMatching.hs
@@ -0,0 +1,426 @@
+{-# LANGUAGE GADTs, RankNTypes, TypeOperators, ViewPatterns, TypeFamilies, FlexibleInstances, FlexibleContexts, TemplateHaskell, UndecidableInstances, ScopedTypeVariables #-}
+
+-- |
+-- Module      : Data.Binding.Hobbits.NuMatching
+-- Copyright   : (c) 2014 Edwin Westbrook, Nicolas Frisby, and Paul Brauner
+--
+-- License     : BSD3
+--
+-- Maintainer  : westbrook@kestrel.edu
+-- Stability   : experimental
+-- Portability : GHC
+--
+-- This module defines the typeclass @'NuMatching' a@, which allows
+-- pattern-matching on the bodies of multi-bindings when their bodies
+-- have type a. To ensure adequacy, the actual machinery of how this
+-- works is hidden from the user, but, for any given (G)ADT @a@, the
+-- user can use the Template Haskell function 'mkNuMatching' to
+-- create a 'NuMatching' instance for @a@.
+--
+
+
+module Data.Binding.Hobbits.NuMatching (
+  NuMatching(..), mkNuMatching, NuMatchingList(..), NuMatching1(..),
+  MbTypeRepr()
+) where
+
+--import Data.Typeable
+import Language.Haskell.TH hiding (Name)
+import qualified Language.Haskell.TH as TH
+import Control.Monad.State
+--import Control.Monad.Identity
+
+import Data.Type.HList
+import Data.Binding.Hobbits.Internal.Name
+import Data.Binding.Hobbits.Internal.Mb
+import Data.Binding.Hobbits.Internal.Closed
+
+
+{-| Just like 'mapNamesPf', except uses the NuMatching class. -}
+mapNames :: NuMatching a => HList Name ctx -> HList Name ctx -> a -> a
+mapNames = mapNamesPf nuMatchingProof
+
+
+{-|
+  Instances of the @'NuMatching' a@ class allow pattern-matching on
+  multi-bindings whose bodies have type @a@, i.e., on multi-bindings
+  of type @'Mb' ctx a@. The structure of this class is mostly hidden
+  from the user; see 'mkNuMatching' to see how to create instances
+  of the @NuMatching@ class.
+-}
+class NuMatching a where
+    nuMatchingProof :: MbTypeRepr a
+
+instance NuMatching (Name a) where
+    nuMatchingProof = MbTypeReprName
+
+instance NuMatching (Cl a) where
+    -- no need to map free variables in a Closed object
+    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\c1 c2 -> id))
+
+instance (NuMatching a, NuMatching b) => NuMatching (a -> b) where
+    nuMatchingProof = MbTypeReprFun nuMatchingProof nuMatchingProof
+
+instance NuMatching a => NuMatching (Mb ctx a) where
+    nuMatchingProof = MbTypeReprMb nuMatchingProof
+
+instance NuMatching Int where
+    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\c1 c2 -> id))
+
+instance NuMatching Integer where
+    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\c1 c2 -> id))
+
+instance NuMatching Char where
+    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\c1 c2 -> id))
+
+instance (NuMatching a, NuMatching b) => NuMatching (a,b) where
+    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\c1 c2 (a,b) -> (mapNames c1 c2 a, mapNames c1 c2 b)))
+
+instance (NuMatching a, NuMatching b, NuMatching c) => NuMatching (a,b,c) where
+    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\c1 c2 (a,b,c) -> (mapNames c1 c2 a, mapNames c1 c2 b, mapNames c1 c2 c)))
+
+instance (NuMatching a, NuMatching b, NuMatching c, NuMatching d) => NuMatching (a,b,c,d) where
+    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\c1 c2 (a,b,c,d) -> (mapNames c1 c2 a, mapNames c1 c2 b, mapNames c1 c2 c, mapNames c1 c2 d)))
+
+instance (NuMatching a, NuMatching b) => NuMatching (Either a b) where
+    nuMatchingProof = MbTypeReprData
+                  (MkMbTypeReprData
+                   $ (\c1 c2 x -> case x of
+                                    Left l -> Left (mapNames c1 c2 l)
+                                    Right r -> Right (mapNames c1 c2 r)))
+
+instance NuMatching a => NuMatching [a] where
+    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\c1 c2 -> map (mapNames c1 c2)))
+
+instance NuMatching (Member c a) where
+    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\c1 c2 -> id))
+
+
+{-
+type family NuMatchingListProof args
+type instance NuMatchingListProof Nil = ()
+type instance NuMatchingListProof (args :> arg) = (NuMatchingListProof args, MbTypeReprData arg)
+
+-- the NuMatchingList class, for saying that NuMatching holds for a context of types
+class NuMatchingList args where
+    nuMatchingListProof :: NuMatchingListProof args
+
+instance NuMatchingList Nil where
+    nuMatchingListProof = ()
+
+instance (NuMatchingList args, NuMatching a) => NuMatchingList (args :> a) where
+    nuMatchingListProof = (nuMatchingListProof, nuMatchingProof)
+-}
+
+data NuMatchingObj a = NuMatching a => NuMatchingObj ()
+
+-- the NuMatchingList class, for saying that NuMatching holds for a context of types
+class NuMatchingList args where
+    nuMatchingListProof :: HList NuMatchingObj args
+
+instance NuMatchingList Nil where
+    nuMatchingListProof = Nil
+
+instance (NuMatchingList args, NuMatching a) => NuMatchingList (args :> a) where
+    nuMatchingListProof = nuMatchingListProof :> NuMatchingObj ()
+
+
+class NuMatching1 f where
+    nuMatchingProof1 :: NuMatching a => NuMatchingObj (f a)
+
+-- README: deriving NuMatching from NuMatching1 leads to overlapping instances
+-- for, e.g., Name a
+{-
+instance (NuMatching1 f, NuMatching a) => NuMatching (f a) where
+    nuMatchingProof = nuMatchingProof1 nuMatchingProof
+-}
+
+instance (NuMatching1 f, NuMatchingList ctx) => NuMatching (HList f ctx) where
+    nuMatchingProof = MbTypeReprData $ MkMbTypeReprData $ helper nuMatchingListProof where
+        helper :: NuMatching1 f =>
+                  HList NuMatchingObj args -> HList Name ctx1 -> HList Name ctx1 ->
+                  HList f args -> HList f args
+        helper Nil c1 c2 Nil = Nil
+        helper (proofs :> NuMatchingObj ()) c1 c2 (elems :> (elem :: f a)) =
+            case nuMatchingProof1 :: NuMatchingObj (f a) of
+              NuMatchingObj () ->
+                  (helper proofs c1 c2 elems) :>
+                  mapNames c1 c2 elem
+
+
+-- now we define some TH to create NuMatchings
+
+natsFrom i = i : natsFrom (i+1)
+
+fst3 :: (a,b,c) -> a
+fst3 (x,_,_) = x
+
+snd3 :: (a,b,c) -> b
+snd3 (_,y,_) = y
+
+thd3 :: (a,b,c) -> c
+thd3 (_,_,z) = z
+
+
+type Names = (TH.Name, TH.Name, TH.Name, TH.Name)
+
+mapNamesType a = [t| forall ctx. HList Name ctx -> HList Name ctx -> $a -> $a |]
+
+{-|
+  Template Haskell function for creating NuMatching instances for (G)ADTs.
+  Typical usage is to include the following line in the source file for
+  (G)ADT @T@ (here assumed to have two type arguments):
+
+> $(mkNuMatching [t| forall a b . T a b |])
+
+  The 'mkNuMatching' call here will create an instance declaration for
+  @'NuMatching' (T a b)@. It is also possible to include a context in the
+  forall type; for example, if we define the 'ID' data type as follows:
+
+> data ID a = ID a
+
+  then we can create a 'NuMatching' instance for it like this:
+
+> $( mkNuMatching [t| NuMatching a => ID a |])
+
+  Note that, when a context is included, the Haskell parser will add
+  the @forall a@ for you.
+-}
+mkNuMatching :: Q Type -> Q [Dec]
+mkNuMatching tQ =
+    do t <- tQ
+       (cxt, cType, tName, constrs, tyvars) <- getMbTypeReprInfoTop t
+       fName <- newName "f"
+       x1Name <- newName "x1"
+       x2Name <- newName "x2"
+       clauses <- mapM (getClause (tName, fName, x1Name, x2Name)) constrs
+       mapNamesT <- mapNamesType (return cType)
+       return [InstanceD
+               cxt (AppT (ConT ''NuMatching) cType)
+               [ValD (VarP 'nuMatchingProof)
+                (NormalB
+                 $ AppE (ConE 'MbTypeReprData)
+                   $ AppE (ConE 'MkMbTypeReprData)
+                         $ LetE [SigD fName
+                                 $ ForallT (map PlainTV tyvars) cxt mapNamesT,
+                                 FunD fName clauses]
+                               (VarE fName)) []]]
+
+       {-
+       return (LetE
+               [SigD fName
+                     (ForallT tyvars reqCxt
+                     $ foldl AppT ArrowT
+                           [foldl AppT (ConT conName)
+                                      (map tyVarToType tyvars)]),
+                FunD fname clauses]
+               (VarE fname))
+        -}
+    where
+      -- extract the name from a TyVarBndr
+      tyBndrToName (PlainTV n) = n
+      tyBndrToName (KindedTV n _) = n
+
+      -- fail for getMbTypeReprInfo
+      getMbTypeReprInfoFail t extraMsg =
+          fail ("mkMbTypeRepr: " ++ show t
+                ++ " is not a type constructor for a (G)ADT applied to zero or more distinct type variables" ++ extraMsg)
+
+      -- get info for conName (top-level call)
+      getMbTypeReprInfoTop t = getMbTypeReprInfo [] [] t t
+
+      -- get info for conName
+      getMbTypeReprInfo ctx tyvars topT (ConT tName) =
+          do info <- reify tName
+             case info of
+               TyConI (DataD _ _ tyvarsReq constrs _) ->
+                   success tyvarsReq constrs
+               TyConI (NewtypeD _ _ tyvarsReq constr _) ->
+                   success tyvarsReq [constr]
+               _ -> getMbTypeReprInfoFail topT (": info for " ++ (show tName) ++ " = " ++ (show info))
+          where
+            success tyvarsReq constrs =
+                let tyvarsRet = if tyvars == [] && ctx == []
+                                then map tyBndrToName tyvarsReq
+                                else tyvars in
+                return (ctx,
+                        foldl AppT (ConT tName) (map VarT tyvars),
+                        tName, constrs, tyvarsRet)
+
+      getMbTypeReprInfo ctx tyvars topT (AppT f (VarT argName)) =
+          if elem argName tyvars then
+              getMbTypeReprInfoFail topT ""
+          else
+              getMbTypeReprInfo ctx (argName:tyvars) topT f
+
+      getMbTypeReprInfo ctx tyvars topT (ForallT _ ctx' t) =
+          getMbTypeReprInfo (ctx ++ ctx') tyvars topT t
+
+      getMbTypeReprInfo ctx tyvars topT t = getMbTypeReprInfoFail topT ""
+
+      -- get the name from a data type
+      getTCtor t = getTCtorHelper t t []
+      getTCtorHelper (ConT tName) topT tyvars = Just (topT, tName, tyvars)
+      getTCtorHelper (AppT t1 (VarT var)) topT tyvars =
+          getTCtorHelper t1 topT (tyvars ++ [var])
+      getTCtorHelper (SigT t1 _) topT tyvars = getTCtorHelper t1 topT tyvars
+      getTCtorHelper _ _ _ = Nothing
+
+      -- get a list of Clauses, one for each constructor in constrs
+      getClauses :: Names -> [Con] -> Q [Clause]
+      getClauses names constrs = mapM (getClause names) constrs
+
+      getClause :: Names -> Con -> Q Clause
+      getClause names (NormalC cName cTypes) =
+          getClauseHelper names (map snd cTypes)
+                          (natsFrom 0)
+                          (\l -> ConP cName (map (VarP . fst3) l))
+                          (\l -> foldl AppE (ConE cName) (map fst3 l))
+
+      getClause names (RecC cName cVarTypes) =
+          getClauseHelper names (map thd3 cVarTypes)
+                         (map fst3 cVarTypes)
+                         (\l -> RecP cName
+                                (map (\(var,_,field) -> (field, VarP var)) l))
+                         (\l -> RecConE cName
+                                (map (\(exp,_,field) -> (field, exp)) l))
+
+      getClause names (InfixC cType1 cName cType2) =
+          undefined -- FIXME
+
+      getClause names (ForallC _ _ con) =  getClause names con
+
+      getClauseHelper :: Names -> [Type] -> [a] ->
+                         ([(TH.Name,Type,a)] -> Pat) ->
+                         ([(Exp,Type,a)] -> Exp) ->
+                         Q Clause
+      getClauseHelper names@(tName, fName, x1Name, x2Name) cTypes cData pFun eFun =
+          do varNames <- mapM (newName . ("x" ++) . show . fst)
+                         $ zip (natsFrom 0) cTypes
+             let varsTypesData = zip3 varNames cTypes cData
+             let expsTypesData = map (mkExpTypeData names) varsTypesData
+             return $ Clause [(VarP x1Name), (VarP x2Name), (pFun varsTypesData)]
+                        (NormalB $ eFun expsTypesData) []
+
+      mkExpTypeData :: Names -> (TH.Name,Type,a) -> (Exp,Type,a)
+      mkExpTypeData (tName, fName, x1Name, x2Name)
+                    (varName, getTCtor -> Just (t, tName', _), cData)
+          | tName == tName' =
+              -- the type of the arg is the same as the (G)ADT we are
+              -- recursing over; apply the recursive function
+              (foldl AppE (VarE fName)
+                         [(VarE x1Name), (VarE x2Name), (VarE varName)],
+               t, cData)
+      mkExpTypeData (tName, fName, x1Name, x2Name) (varName, t, cData) =
+          -- the type of the arg is not the same as the (G)ADT; call mapNames
+          (foldl AppE (VarE 'mapNames)
+                     [(VarE x1Name), (VarE x2Name), (VarE varName)],
+           t, cData)
+
+-- FIXME: old stuff below
+
+type CxtStateQ a = StateT Cxt Q a
+
+-- create a MkMbTypeReprData for a (G)ADT
+mkMkMbTypeReprDataOld :: Q TH.Name -> Q Exp
+mkMkMbTypeReprDataOld conNameQ =
+    do conName <- conNameQ
+       (cxt, name, tyvars, constrs) <- getMbTypeReprInfo conName
+       (clauses, reqCxt) <- runStateT (getClauses cxt name tyvars constrs) []
+       fname <- newName "f"
+       return (LetE
+               [SigD fname
+                     (ForallT tyvars reqCxt
+                     $ foldl AppT ArrowT
+                           [foldl AppT (ConT conName)
+                                      (map tyVarToType tyvars)]),
+                FunD fname clauses]
+               (VarE fname))
+    where
+      -- convert a TyVar to a Name
+      tyVarToType (PlainTV n) = VarT n
+      tyVarToType (KindedTV n _) = VarT n
+
+      -- get info for conName
+      getMbTypeReprInfo conName =
+          reify conName >>= \info ->
+              case info of
+                TyConI (DataD cxt name tyvars constrs _) ->
+                    return (cxt, name, tyvars, constrs)
+                _ -> fail ("mkMkMbTypeReprData: " ++ show conName
+                           ++ " is not a (G)ADT")
+      {-
+      -- report failure
+      getMbTypeReprInfoFail t =
+          fail ("mkMkMbTypeReprData: " ++ show t
+                ++ " is not a fully applied (G)ADT")
+
+      getMbTypeReprInfo (ConT conName) topT =
+          reify conName >>= \info ->
+              case info of
+                TyConI (DataD cxt name tyvars constrs _) ->
+                    return (cxt, name, tyvars, constrs)
+                _ -> getMbTypeReprInfoFail topT
+      getMbTypeReprInfo (AppT t _) topT = getMbTypeReprInfo t topT
+      getMbTypeReprInfo (SigT t _) topT = getMbTypeReprInfo t topT
+      getMbTypeReprInfo _ topT = getMbTypeReprInfoFail topT
+       -}
+
+      -- get a list of Clauses, one for each constructor in constrs
+      getClauses :: Cxt -> TH.Name -> [TyVarBndr] -> [Con] -> CxtStateQ [Clause]
+      getClauses cxt name tyvars constrs =
+          mapM (getClause cxt name tyvars []) constrs
+
+      getClause :: Cxt -> TH.Name -> [TyVarBndr] -> [TyVarBndr] -> Con ->
+                   CxtStateQ Clause
+      getClause cxt name tyvars locTyvars (NormalC cName cTypes) =
+          getClauseHelper cxt name tyvars locTyvars (map snd cTypes)
+                          (natsFrom 0)
+                          (\l -> ConP cName (map (VarP . fst3) l))
+                          (\l -> foldl AppE (ConE cName) (map (VarE . fst3) l))
+
+      getClause cxt name tyvars locTyvars (RecC cName cVarTypes) =
+          getClauseHelper cxt name tyvars locTyvars (map thd3 cVarTypes)
+                         (map fst3 cVarTypes)
+                         (\l -> RecP cName
+                                (map (\(var,_,field) -> (field, VarP var)) l))
+                         (\l -> RecConE cName
+                                (map (\(var,_,field) -> (field, VarE var)) l))
+
+      getClause cxt name tyvars locTyvars (InfixC cType1 cName cType2) =
+          undefined -- FIXME
+
+      getClause cxt name tyvars locTyvars (ForallC tyvars2 cxt2 con) =
+          getClause (cxt ++ cxt2) name tyvars (locTyvars ++ tyvars2) con
+
+      getClauseHelper :: Cxt -> TH.Name -> [TyVarBndr] -> [TyVarBndr] ->
+                         [Type] -> [a] ->
+                         ([(TH.Name,Type,a)] -> Pat) ->
+                         ([(TH.Name,Type,a)] -> Exp) ->
+                         CxtStateQ Clause
+      getClauseHelper cxt name tyvars locTyvars cTypes cData pFun eFun =
+          do varNames <- mapM (lift . newName . ("x" ++) . show . fst)
+                         $ zip (natsFrom 0) cTypes
+             () <- ensureCxt cxt locTyvars cTypes
+             let varsTypesData = zip3 varNames cTypes cData
+             return $ Clause [(pFun varsTypesData)]
+                        (NormalB $ eFun varsTypesData) []
+
+      -- ensure that MbTypeRepr a holds for each type a in cTypes
+      ensureCxt :: Cxt -> [TyVarBndr] -> [Type] -> CxtStateQ ()
+      ensureCxt cxt locTyvars cTypes =
+          foldM (const (ensureCxt1 cxt locTyvars)) () cTypes
+
+      -- FIXME: it is not possible (or, at least, not easy) to determine
+      -- if MbTypeRepr a is implied from a current Cxt... so we just add
+      -- everything we need to the returned Cxt, except for 
+      ensureCxt1 :: Cxt -> [TyVarBndr] -> Type -> CxtStateQ ()
+      ensureCxt1 cxt locTyvars t = undefined
+      {-
+      ensureCxt1 cxt locTyvars t = do
+        curCxt = get
+        let fullCxt = cxt ++ curCxt
+        isOk <- isMbTypeRepr fullCxt 
+
+      isMbTypeRepr 
+       -}
diff --git a/Data/Binding/Hobbits/QQ.hs b/Data/Binding/Hobbits/QQ.hs
--- a/Data/Binding/Hobbits/QQ.hs
+++ b/Data/Binding/Hobbits/QQ.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TemplateHaskell, FlexibleContexts #-}
 
 -- |
 -- Module      : Data.Binding.Hobbits.QQ
@@ -25,10 +25,6 @@
 
 module Data.Binding.Hobbits.QQ (nuP, clP, clNuP) where
 
-import qualified Data.Binding.Hobbits.InternalUtilities as IU
-import Data.Binding.Hobbits.Internal (Mb(..), Cl(..))
-import Data.Binding.Hobbits.PatternParser (parsePattern)
-
 import Language.Haskell.TH.Syntax as TH
 import Language.Haskell.TH.Ppr as TH
 import Language.Haskell.TH.Quote
@@ -37,60 +33,79 @@
 import Control.Monad.Writer (runWriterT, tell)
 import Data.Monoid (Any(..))
 
-
+import qualified Data.Binding.Hobbits.Internal.Utilities as IU
+import Data.Binding.Hobbits.Internal.Mb
+import Data.Binding.Hobbits.Internal.Closed
+import Data.Binding.Hobbits.PatternParser (parsePattern)
+import Data.Binding.Hobbits.NuMatching
 
 
+-- | Helper function to apply an expression to multiple arguments
+appEMulti :: Exp -> [Exp] -> Exp
+appEMulti = foldl AppE
 
+-- | Helper function to apply the (.) operator on expressions
 compose :: Exp -> Exp -> Exp
 compose f g = VarE '(.) `AppE` f `AppE` g
 
+-- | @patQQ str pat@ builds a quasi-quoter named @str@ that parses
+-- | patterns with @pat@
+patQQ :: String -> (String -> Q Pat) -> QuasiQuoter
 patQQ n pat = QuasiQuoter (err "Exp") pat (err "Type") (err "Decs")
   where err s = error $ "QQ `" ++ n ++ "' is for patterns, not " ++ s ++ "."
 
 
-
-
-
+-- | A @WrapKit@ specifies a transformation to be applied to variables
+-- | in a Template Haskell patterns, as follows:
+--
+-- * @_varView@ gives an expression for a function to be applied, as a
+--   view pattern, to variables before matching them, including to
+--   variables bound by @\@@ patterns;
+--
+-- * @_asXform@ gives a function to transform the bodies of \@
+--   patterns, i.e., this function is applied to @p@ in pattern @x\@p@;
+--
+-- * @_topXform@ gives a function to transform the whole pattern after
+--    @_varView@ and/or @_asXform@ have been applied to sub-patterns;
+--    as the first argument, @_topXform@ also takes a flag indicating
+--    whether any transformations have been applied to sub-patterns.
+--
 data WrapKit =
-  -- _add adds structure just before binding the name (i.e. on VarP)
-  -- _rm  removes structure that was added for the @ patterns
-  -- _top removes structure at the top of the whole pattern
-  WrapKit {_add :: Exp, _rm :: Pat -> Pat, _top :: Bool -> Pat -> Pat}
+  WrapKit {_varView :: Exp, _asXform :: Pat -> Pat, _topXform :: Bool -> Pat -> Pat}
 
-outsideKit (WrapKit {_add = addO, _rm = rmO, _top = topO})
-           (WrapKit {_add = addI, _rm = rmI, _top = topI}) =
-  WrapKit {_add = addO `compose` addI,
-           _rm = rmO . rmI,
-           _top = \b -> topO b . topI b}
+-- | Combine two WrapKits, composing the individual components
+combineWrapKits :: WrapKit -> WrapKit -> WrapKit
+combineWrapKits (WrapKit {_varView = varViewO, _asXform = asXformO, _topXform = topXformO})
+           (WrapKit {_varView = varViewI, _asXform = asXformI, _topXform = topXformI}) =
+  WrapKit {_varView = varViewO `compose` varViewI,
+           _asXform = asXformO . asXformI,
+           _topXform = \b -> topXformO b . topXformI b}
 
--- wrapVars changes the types of names bound in a pattern
+-- | Apply a 'WrapKit' to a pattern
 wrapVars :: Monad m => WrapKit -> Pat -> m Pat
-wrapVars (WrapKit {_add = add, _rm = rm, _top = top}) pat = do
-  (pat', Any usedAdd) <- runWriterT m
-  return $ top usedAdd pat'
+wrapVars (WrapKit {_varView = varView, _asXform = asXform, _topXform = topXform}) pat = do
+  (pat', Any usedVarView) <- runWriterT m
+  return $ topXform usedVarView pat'
   where
     m = IU.everywhereButM (SYB.mkQ False isExp) (SYB.mkM w) pat
       where isExp :: Exp -> Bool
             -- don't recur into the expression part of view patterns
             isExp _ = True
 
-    -- this should be called if the 'add' function is ever used
+    -- this should be called if the 'varView' function is ever used
     hit x = tell (Any True) >> return x
 
     -- wraps up bound names
-    w p@VarP{} = hit $ ViewP add p
+    w p@VarP{} = hit $ ViewP varView p
     -- wraps for the bound name, then immediately unwraps
     -- for the rest of the pattern
-    w (AsP v p) = hit $ ViewP add $ AsP v $ rm p
+    w (AsP v p) = hit $ ViewP varView $ AsP v $ asXform p
     -- requires the expression to be closed
     w (ViewP (VarE n) p) = return $ ViewP (VarE 'unCl `AppE` VarE n) p
     w (ViewP e _) = fail $ "view function must be a single name: `" ++ show (TH.ppr e) ++ "'"
     w p = return p
 
-
-
-
-
+-- | Parse a pattern from a string, using 'parsePattern'
 parseHere :: String -> Q Pat
 parseHere s = do
   fn <- loc_filename `fmap` location
@@ -100,45 +115,34 @@
     Right p -> return p
 
 
-
-
-
+-- | A helper function used to ensure two multi-bindings have the same contexts
 same_ctx :: Mb ctx a -> Mb ctx b -> Mb ctx b
 same_ctx _ x = x
 
-nuKit mb ln = WrapKit {_add = add, _rm = rm, _top = top} where
-  add = (VarE 'same_ctx `AppE` VarE mb) `compose`
-        (ConE 'MkMb     `AppE` VarE ln)
-
-  rm p = ConP 'MkMb [WildP, p]
-
-  top b p = if b then AsP mb $ ConP 'MkMb [VarP ln, p] else rm p
-
-
-
-
+-- | Builds a 'WrapKit' for parsing patterns that match over 'Mb'.
+-- | Takes two fresh names as arguments.
+nuKit :: TH.Name -> TH.Name -> WrapKit
+nuKit topVar namesVar = WrapKit {_varView = varView, _asXform = asXform, _topXform = topXform} where
+  varView = (VarE 'same_ctx `AppE` VarE topVar) `compose`
+        (appEMulti (ConE 'MkMbPair) [VarE 'nuMatchingProof, VarE namesVar])
+  asXform p = ViewP (VarE 'ensureFreshPair) (TupP [WildP, p])
+  topXform b p = if b then AsP topVar $ ViewP (VarE 'ensureFreshPair) (TupP [VarP namesVar, p]) else asXform p
 
+-- | Quasi-quoter for patterns that match over 'Mb'
 nuP = patQQ "nuP" $ \s -> do
-  mb <- newName "mb"
-  ln <- newName "bs"
-
-  parseHere s >>= wrapVars (nuKit mb ln)
-
-
-
-
+  topVar <- newName "topMb"
+  namesVar <- newName "topNames"
+  parseHere s >>= wrapVars (nuKit topVar namesVar)
 
-clKit = WrapKit {_add = ConE 'Cl, _rm = rm, _top = const rm}
-  where rm p = ConP 'Cl [p]
+-- | Builds a 'WrapKit' for parsing patterns that match over 'Cl'
+clKit = WrapKit {_varView = ConE 'Cl, _asXform = asXform, _topXform = const asXform}
+  where asXform p = ConP 'Cl [p]
 
+-- | Quasi-quoter for patterns that match over 'Cl', built using 'clKit'
 clP = patQQ "clP" $ (>>= wrapVars clKit) . parseHere
 
-
-
-
-
+-- | Quasi-quoter for patterhs that match over @'Cl' ('Mb' ctx a)@
 clNuP = patQQ "clNuP" $ \s -> do
-  mb <- newName "mb"
-  ln <- newName "bs"
-
-  parseHere s >>= wrapVars (clKit `outsideKit` nuKit mb ln)
+  topVar <- newName "topMb"
+  namesVar <- newName "topNames"
+  parseHere s >>= wrapVars (clKit `combineWrapKits` nuKit topVar namesVar)
diff --git a/Data/Type/HList.hs b/Data/Type/HList.hs
new file mode 100644
--- /dev/null
+++ b/Data/Type/HList.hs
@@ -0,0 +1,203 @@
+{-# LANGUAGE TypeOperators, EmptyDataDecls, RankNTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE GADTs #-}
+
+-- |
+-- Module      : Data.Type.HList
+-- Copyright   : (c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul Brauner
+--
+-- License     : BSD3
+--
+-- Maintainer  : westbrook@galois.com
+-- Stability   : experimental
+-- Portability : GHC
+--
+-- A /type list/ contains types as elements. We use GADT proofs terms to
+-- establish membership and append relations. A @Data.Type.HList.HList@ @f@
+-- is a vector indexed by a type list, where @f :: * -> *@ is applied to each
+-- type element.
+
+module Data.Type.HList where
+
+import Data.Type.Equality ((:~:)(..))
+import Data.Proxy (Proxy(..))
+import Data.Functor.Constant
+import Data.Typeable
+
+-------------------------------------------------------------------------------
+-- type-level lists
+-------------------------------------------------------------------------------
+
+data Nil deriving Typeable
+data r :> a deriving Typeable; infixl 5 :>
+
+type family (r1 :++: r2); infixr 5 :++:
+type instance r :++: Nil = r
+type instance r1 :++: r2 :> a = (r1 :++: r2) :> a
+
+proxyCons :: Proxy r -> f a -> Proxy (r :> a)
+proxyCons _ _ = Proxy
+
+
+-------------------------------------------------------------------------------
+-- proofs of membership in a type-level list
+-------------------------------------------------------------------------------
+
+{-|
+  A @Member ctx a@ is a \"proof\" that the type @a@ is in the type
+  list @ctx@, meaning that @ctx@ equals
+
+>  t0 ':>' a ':>' t1 ':>' ... ':>' tn
+
+  for some types @t0,t1,...,tn@.
+-}
+data Member ctx a where
+  Member_Base :: Member (ctx :> a) a
+  Member_Step :: Member ctx a -> Member (ctx :> b) a
+  deriving Typeable
+
+instance Show (Member r a) where showsPrec p = showsPrecMember (p > 10)
+
+showsPrecMember :: Bool -> Member ctx a -> ShowS
+showsPrecMember _ Member_Base = showString "Member_Base"
+showsPrecMember p (Member_Step prf) = showParen p $
+  showString "Member_Step" . showsPrec 10 prf
+
+--toEq :: Member (Nil :> a) b -> b :~: a
+--toEq Member_Base = Refl
+--toEq _ = error "Should not happen! (toEq)"
+
+weakenMemberL :: Proxy r1 -> Member r2 a -> Member (r1 :++: r2) a
+weakenMemberL _ Member_Base = Member_Base
+weakenMemberL tag (Member_Step mem) = Member_Step (weakenMemberL tag mem)
+
+membersEq :: Member ctx a -> Member ctx b -> Maybe (a :~: b)
+membersEq Member_Base Member_Base = Just Refl
+membersEq (Member_Step mem1) (Member_Step mem2) = membersEq mem1 mem2
+membersEq _ _ = Nothing
+
+
+------------------------------------------------------------
+-- proofs that one list equals the append of two others
+------------------------------------------------------------
+
+{-|
+  An @Append ctx1 ctx2 ctx@ is a \"proof\" that @ctx = ctx1 ':++:' ctx2@.
+-}
+data Append ctx1 ctx2 ctx where
+  Append_Base :: Append ctx Nil ctx
+  Append_Step :: Append ctx1 ctx2 ctx -> Append ctx1 (ctx2 :> a) (ctx :> a)
+
+-- -- | Appends two 'Append' proofs.
+-- trans ::
+--   Append ctx1 ctx2 ex_ctx -> Append ex_ctx ctx3 ctx -> Append ctx1 (ctx2 :++: ctx3) ctx
+-- trans app Append_Base = app
+-- trans app (Append_Step app') = Append_Step (trans app app')
+
+-- -- | Returns a proof that ctx :~: ctx1 :++: ctx2
+-- appendPf :: Append ctx1 ctx2 ctx -> (ctx :~: ctx1 :++: ctx2)
+-- appendPf Append_Base = Refl
+-- appendPf (Append_Step app) = case appendPf app of Refl -> Refl
+
+-- -- | Returns the length of an 'Append' proof.
+-- length :: Append ctx1 ctx2 ctx3 -> Int
+-- length Append_Base = 0
+-- length (Append_Step app) = 1 + Data.Type.List.Proof.Append.length app
+
+-------------------------------------------------------------------------------
+-- Heterogeneous lists
+-------------------------------------------------------------------------------
+
+{-|
+  A @HList f c@ is a vector with exactly one element of type @f a@ for
+  each type @a@ in the type list @c@.
+-}
+data HList f c where
+  Nil :: HList f Nil -- Creates an empty vector
+  (:>) :: HList f c -> f a -> HList f (c :> a) -- Appends an element to the end of a vector
+
+-- | Create an empty 'HList' vector.
+empty :: HList f Nil
+empty = Nil
+
+-- | Create a singleton 'HList' vector.
+singleton :: f a -> HList f (Nil :> a)
+singleton x = Nil :> x
+
+-- | Look up an element of a 'HList' vector using a 'Member' proof.
+hlistLookup :: Member c a -> HList f c -> f a
+hlistLookup Member_Base (_ :> x) = x
+hlistLookup (Member_Step mem') (mc :> _) = hlistLookup mem' mc
+--hlistLookup _ _ = error "Should not happen! (hlistLookup)"
+
+-- | Map a function on all elements of a 'HList' vector.
+mapHList :: (forall x. f x -> g x) -> HList f c -> HList g c
+mapHList _ Nil = Nil
+mapHList f (mc :> x) = mapHList f mc :> f x
+
+-- | Map a binary function on all pairs of elements of two 'HList' vectors.
+mapHList2 :: (forall x. f x -> g x -> h x) -> HList f c -> HList g c -> HList h c
+mapHList2 _ Nil Nil = Nil
+mapHList2 f (xs :> x) (ys :> y) = mapHList2 f xs ys :> f x y
+mapHList2 _ _ _ = error "Something is terribly wrong in mapHList2: this case should not happen!"
+
+-- | Append two 'HList' vectors.
+appendHList :: HList f c1 -> HList f c2 -> HList f (c1 :++: c2)
+appendHList mc Nil = mc
+appendHList mc1 (mc2 :> x) = appendHList mc1 mc2 :> x
+
+-- -- | Append two 'HList' vectors.
+-- appendWithPf :: Append c1 c2 c -> HList f c1 -> HList f c2 -> HList f c
+-- appendWithPf Append_Base mc Nil = mc
+-- appendWithPf (Append_Step app) mc1 (mc2 :> x) = appendWithPf app mc1 mc2 :> x
+-- appendWithPf  _ _ _ = error "Something is terribly wrong in appendWithPf: this case should not happen!"
+
+-- | Make an 'Append' proof from any 'HList' vector for the second
+-- argument of the append.
+mkAppend :: HList f c2 -> Append c1 c2 (c1 :++: c2)
+mkAppend Nil = Append_Base
+mkAppend (c :> _) = Append_Step (mkAppend c)
+
+-- | A version of 'mkAppend' that takes in a 'Proxy' argument.
+mkMonoAppend :: Proxy c1 -> HList f c2 -> Append c1 c2 (c1 :++: c2)
+mkMonoAppend _ = mkAppend
+
+-- | The inverse of 'mkAppend', that builds an 'HList' from an 'Append'
+proxiesFromAppend :: Append c1 c2 c -> HList Proxy c2
+proxiesFromAppend Append_Base = Nil
+proxiesFromAppend (Append_Step a) = proxiesFromAppend a :> Proxy
+
+-- | Split an 'HList' vector into two pieces. The first argument is a
+-- phantom argument that gives the form of the first list piece.
+splitHList :: (c ~ (c1 :++: c2)) => Proxy c1 -> HList any c2 -> HList f c -> (HList f c1, HList f c2)
+splitHList _ Nil mc = (mc, Nil)
+splitHList _ (any :> _) (mc :> x) = (mc1, mc2 :> x)
+  where (mc1, mc2) = splitHList Proxy any mc
+--split _ _ = error "Should not happen! (Map.split)"
+
+-- | Create a vector of proofs that each type in @c@ is a 'Member' of @c@.
+members :: HList f c -> HList (Member c) c
+members Nil = Nil
+members (c :> _) = mapHList Member_Step (members c) :> Member_Base
+
+-- -- | Replace a single element of a 'HList' vector.
+-- replace :: HList f c -> Member c a -> f a -> HList f c
+-- replace (xs :> _) Member_Base y = xs :> y
+-- replace (xs :> x) (Member_Step memb) y = replace xs memb y :> x
+-- replace _ _ _ = error "Should not happen! (Map.replace)"
+
+-- | Convert an HList to a list
+hlistToList :: HList (Constant a) c -> [a]
+hlistToList Nil = []
+hlistToList (xs :> Constant x) = hlistToList xs ++ [x]
+
+-- | A type-class which ensures that ctx is a valid context, i.e., has
+-- | the form (Nil :> t1 :> ... :> tn) for some types t1 through tn
+class TypeCtx ctx where
+  typeCtxProxies :: HList Proxy ctx
+
+instance TypeCtx Nil where
+  typeCtxProxies = Nil
+
+instance TypeCtx ctx => TypeCtx (ctx :> a) where
+  typeCtxProxies = typeCtxProxies :> Proxy
diff --git a/Data/Type/List.hs b/Data/Type/List.hs
deleted file mode 100644
--- a/Data/Type/List.hs
+++ /dev/null
@@ -1,35 +0,0 @@
-{-# LANGUAGE TypeOperators, EmptyDataDecls #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE GADTs #-}
-
--- |
--- Module      : Data.Type.List
--- Copyright   : (c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul Brauner
---
--- License     : BSD3
---
--- Maintainer  : emw4@rice.edu
--- Stability   : experimental
--- Portability : GHC
---
--- A /type list/ contains types as elements. We use GADT proofs terms to
--- establish membership and append relations. A @Data.Type.List.Map.MapC@ @f@
--- is a vector indexed by a type list, where @f :: * -> *@ is applied to each
--- type element.
-
-module Data.Type.List (
-  module Data.Type.List.List, -- | Type-level nil, cons, and ++
-  module Data.Type.List.Map, -- | Vectors parameterized by a @* -> *@ and indexed by a type list
-  module Data.Type.List.Proof.Member, -- | Membership functions and proofs
-  module Data.Type.List.Proof.Append, -- | Append functions and proofs
-  module Data.Type.Equality,
-  module Data.Proxy
-  ) where
-
-import Data.Type.List.List
-import Data.Type.List.Map (MapC(..))
-import Data.Type.List.Proof.Member (Member(..))
-import Data.Type.List.Proof.Append (Append(..))
-
-import Data.Type.Equality ((:=:)(..))
-import Data.Proxy (Proxy(..))
diff --git a/Data/Type/List/List.hs b/Data/Type/List/List.hs
deleted file mode 100644
--- a/Data/Type/List/List.hs
+++ /dev/null
@@ -1,35 +0,0 @@
-{-# LANGUAGE EmptyDataDecls #-}
-{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE DeriveDataTypeable #-}
-
--- |
--- Module      : Data.Type.List.List
--- Copyright   : (c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul Brauner
---
--- License     : BSD3
---
--- Maintainer  : emw4@rice.edu
--- Stability   : experimental
--- Portability : GHC
---
--- The type-level constructors of type lists.
-
-module Data.Type.List.List where
-
-import Data.Proxy (Proxy(..))
-import Data.Typeable
-
--------------------------------------------------------------------------------
--- type-level lists
--------------------------------------------------------------------------------
-
-data Nil deriving Typeable
-data r :> a deriving Typeable; infixl 5 :>
-
-type family (r1 :++: r2); infixr 5 :++:
-type instance r :++: Nil = r
-type instance r1 :++: r2 :> a = (r1 :++: r2) :> a
-
-proxyCons :: Proxy r -> f a -> Proxy (r :> a)
-proxyCons _ _ = Proxy
diff --git a/Data/Type/List/Map.hs b/Data/Type/List/Map.hs
deleted file mode 100644
--- a/Data/Type/List/Map.hs
+++ /dev/null
@@ -1,101 +0,0 @@
-{-# LANGUAGE GADTs, TypeOperators, RankNTypes #-}
-
--- |
--- Module      : Data.Type.List.Map
--- Copyright   : (c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul Brauner
---
--- License     : BSD3
---
--- Maintainer  : emw4@rice.edu
--- Stability   : experimental
--- Portability : GHC
---
--- Vectors indexed by a type list
-
-module Data.Type.List.Map where
-
-import Data.Type.List.List
-import Data.Type.List.Proof.Append (Append(..))
-import Data.Type.List.Proof.Member (Member(..))
-import Data.Proxy (Proxy(..))
---import Data.Typeable
-
-import Data.Functor.Constant
-
--------------------------------------------------------------------------------
--- a vector of functor values, indexed by an List
--------------------------------------------------------------------------------
-
-{-|
-  A @MapC f c@ is a vector with exactly one element of type @f a@ for
-  each type @a@ in the type list @c@.
--}
-data MapC f c where
-  Nil :: MapC f Nil -- Creates an empty vector
-  (:>) :: MapC f c -> f a -> MapC f (c :> a) -- Appends an element to the end of a vector
-
--- | Create an empty 'MapC' vector.
-empty :: MapC f Nil
-empty = Nil
-
--- | Create a singleton 'MapC' vector.
-singleton :: f a -> MapC f (Nil :> a)
-singleton x = Nil :> x
-
--- | Look up an element of a 'MapC' vector using a 'Member' proof.
-lookup :: Member c a -> MapC f c -> f a
-lookup Member_Base (_ :> x) = x
-lookup (Member_Step mem') (mc :> _) = Data.Type.List.Map.lookup mem' mc
-lookup _ _ = error "Should not happen! (Map.lookup)"
-
--- | Map a function to all elements of a 'MapC' vector.
-mapC :: (forall x. f x -> g x) -> MapC f c -> MapC g c
-mapC _ Nil = Nil
-mapC f (mc :> x) = mapC f mc :> f x
-
--- | Map a binary function to all pairs of elements of two 'MapC' vectors.
-mapC2 :: (forall x. f x -> g x -> h x) -> MapC f c -> MapC g c -> MapC h c
-mapC2 _ Nil Nil = Nil
-mapC2 f (xs :> x) (ys :> y) = mapC2 f xs ys :> f x y
-
--- | Append two 'MapC' vectors.
-append :: MapC f c1 -> MapC f c2 -> MapC f (c1 :++: c2)
-append mc Nil = mc
-append mc1 (mc2 :> x) = append mc1 mc2 :> x
-
--- | Make an 'Append' proof from any 'MapC' vector for the second
--- argument of the append.
-mkAppend :: MapC f c2 -> Append c1 c2 (c1 :++: c2)
-mkAppend Nil = Append_Base
-mkAppend (c :> _) = Append_Step (mkAppend c)
-
--- | A version of 'mkAppend' that takes in a 'Proxy' argument.
-mkMonoAppend :: Proxy c1 -> MapC f c2 -> Append c1 c2 (c1 :++: c2)
-mkMonoAppend _ = mkAppend
-
--- | Split a 'MapC' vector into two pieces.
-split :: Append c1 c2 c -> MapC f c -> (MapC f c1, MapC f c2)
-split Append_Base mc = (mc, Nil)
-split (Append_Step app) (mc :> x) = (mc1, mc2 :> x)
-  where (mc1, mc2) = split app mc
-split _ _ = error "Should not happen! (Map.split)"
-
--- | Create a 'Proxy' object for the type list of a 'MapC' vector.
-proxy :: MapC f c -> Proxy c
-proxy _ = Proxy
-
--- | Create a vector of proofs that each type in @c@ is a 'Member' of @c@.
-members :: MapC f c -> MapC (Member c) c
-members Nil = Nil
-members (c :> _) =
-  mapC Member_Step (members c) :> Member_Base
-
--- | Replace a single element of a 'MapC' vector.
-replace :: MapC f c -> Member c a -> f a -> MapC f c
-replace (xs :> _) Member_Base y = xs :> y
-replace (xs :> x) (Member_Step memb) y = replace xs memb y :> x
-
--- | Convert a MapC to a list
-mapCToList :: MapC (Constant a) c -> [a]
-mapCToList Nil = []
-mapCToList (xs :> Constant x) = mapCToList xs ++ [x]
diff --git a/Data/Type/List/Proof/Append.hs b/Data/Type/List/Proof/Append.hs
deleted file mode 100644
--- a/Data/Type/List/Proof/Append.hs
+++ /dev/null
@@ -1,46 +0,0 @@
-{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE GADTs #-}
-
--- |
--- Module      : Data.Type.List.Proof.Append
--- Copyright   : (c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul Brauner
---
--- License     : BSD3
---
--- Maintainer  : emw4@rice.edu
--- Stability   : experimental
--- Portability : GHC
---
--- Proofs regarding a type list as an append of two others.
-
-module Data.Type.List.Proof.Append where
-
-import Data.Type.List.List
-import Data.Type.Equality ((:=:)(..))
-
-------------------------------------------------------------
--- proofs about appended lists
-------------------------------------------------------------
-
-{-|
-  An @Append ctx1 ctx2 ctx@ is a \"proof\" that @ctx = ctx1 ':++:' ctx2@.
--}
-data Append ctx1 ctx2 ctx where
-  Append_Base :: Append ctx Nil ctx
-  Append_Step :: Append ctx1 ctx2 ctx -> Append ctx1 (ctx2 :> a) (ctx :> a)
-
--- | Appends two 'Append' proofs.
-trans ::
-  Append ctx1 ctx2 ex_ctx -> Append ex_ctx ctx3 ctx -> Append ctx1 (ctx2 :++: ctx3) ctx
-trans app Append_Base = app
-trans app (Append_Step app') = Append_Step (trans app app')
-
--- | Returns a proof that ctx :=: ctx1 :++: ctx2
-appendPf :: Append ctx1 ctx2 ctx -> (ctx :=: ctx1 :++: ctx2)
-appendPf Append_Base = Refl
-appendPf (Append_Step app) = case appendPf app of Refl -> Refl
-
--- | Returns the length of an 'Append' proof.
-length :: Append ctx1 ctx2 ctx3 -> Int
-length Append_Base = 0
-length (Append_Step app) = 1 + Data.Type.List.Proof.Append.length app
diff --git a/Data/Type/List/Proof/Member.hs b/Data/Type/List/Proof/Member.hs
deleted file mode 100644
--- a/Data/Type/List/Proof/Member.hs
+++ /dev/null
@@ -1,85 +0,0 @@
-{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE DeriveDataTypeable #-}
-
--- |
--- Module      : Data.Type.List.Proof.Member
--- Copyright   : (c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul Brauner
---
--- License     : BSD3
---
--- Maintainer  : emw4@rice.edu
--- Stability   : experimental
--- Portability : GHC
---
--- Proofs regarding membership of a type in a type list.
-
-module Data.Type.List.Proof.Member (
-  -- * Abstract data types
-  Member(..),
-  -- * Operators on 'Member' proofs
-  toEq, weakenL, same, weakenR, split
-  ) where
-
-import Data.Type.List.List
-import Data.Type.List.Proof.Append
-
-import Data.Type.Equality ((:=:)(..))
-import Data.Proxy (Proxy(..))
-import Data.Typeable
-
-import Unsafe.Coerce
-
--------------------------------------------------------------------------------
--- proof of membership
--------------------------------------------------------------------------------
-
-{-|
-  A @Member ctx a@ is a \"proof\" that the type @a@ is in the type
-  list @ctx@, meaning that @ctx@ equals
-
->  t0 ':>' a ':>' t1 ':>' ... ':>' tn
-
-  for some types @t0,t1,...,tn@.
--}
-data Member ctx a where
-  Member_Base :: Member (ctx :> a) a
-  Member_Step :: Member ctx a -> Member (ctx :> b) a
-  deriving Typeable
-
-instance Show (Member r a) where showsPrec p = showsPrecMember (p > 10)
-
-showsPrecMember _ Member_Base = showString "Member_Base"
-showsPrecMember p (Member_Step prf) = showParen p $
-  showString "Member_Step" . showsPrec 10 prf
-
-toEq :: Member (Nil :> a) b -> b :=: a
-toEq Member_Base = Refl
-toEq _ = error "Should not happen! (toEq)"
-
-weakenL :: Proxy r1 -> Member r2 a -> Member (r1 :++: r2) a
-weakenL _    Member_Base = Member_Base
-weakenL tag (Member_Step mem) = Member_Step (weakenL tag mem)
-
-same :: Member r a -> Member r b -> Maybe (a :=: b)
-same Member_Base Member_Base = Just $ unsafeCoerce Refl
-same (Member_Step mem1) (Member_Step mem2) = same mem1 mem2
-same _ _ = Nothing
-
--------------------------------------------------------------------------------
--- relations between Member and Append
--------------------------------------------------------------------------------
-
-weakenR :: Member r1 a -> Append r1 r2 r -> Member r a
-weakenR mem Append_Base = mem
-weakenR mem (Append_Step app) = Member_Step (weakenR mem app)
-
-split ::
-  Append r1 r2 r -> Member r a -> Either (Member r1 a) (Member r2 a)
-split app mem = case app of
-  Append_Base -> Left mem
-  Append_Step app' -> case mem of
-    Member_Base -> Right Member_Base
-    Member_Step mem' -> case split app' mem' of
-      Left prf -> Left prf
-      Right prf -> Right (Member_Step prf)
diff --git a/hobbits.cabal b/hobbits.cabal
--- a/hobbits.cabal
+++ b/hobbits.cabal
@@ -1,5 +1,5 @@
 Name:                hobbits
-Version:             1.1.1
+Version:             1.2
 Synopsis:            A library for canonically representing terms with binding
 
 Description: A library for canonically representing terms with binding via a
@@ -9,7 +9,7 @@
 License:             BSD3
 License-file:        LICENSE
 Author:              Eddy Westbrook, Nicolas Frisby, Paul Brauner
-Maintainer:          emw4@rice.edu
+Maintainer:          westbrook@galois.com
 
 Category:            Data Structures
 
@@ -17,27 +17,23 @@
 Build-Type:    Simple
 
 Library
-  Build-Depends: base >= 4 && < 5
-  Build-Depends: template-haskell >= 2.5 && < 2.9
+  Build-Depends: base >= 4.7 && < 4.9
+  Build-Depends: template-haskell >= 2.9 && < 2.11
 
   Build-Depends: syb
   Build-Depends: mtl
 
-  Build-Depends: type-equality, tagged
+  Build-Depends: tagged
   Build-Depends: deepseq
 
-  Build-Depends: haskell-src-meta >= 0.5.1.1, haskell-src-exts,
+  Build-Depends: haskell-src-exts >= 1.17.1 && < 1.18, haskell-src-meta,
                  th-expand-syns >= 0.3 && < 0.4, transformers
 
   GHC-Options: -fwarn-incomplete-patterns -fwarn-unused-imports
 
   Extensions: CPP
 
-  Exposed-Modules: Data.Type.List,
-                   Data.Type.List.List,
-                   Data.Type.List.Map,
-                   Data.Type.List.Proof.Append,
-                   Data.Type.List.Proof.Member,
+  Exposed-Modules: Data.Type.HList,
 
                    Data.Binding.Hobbits,
                    Data.Binding.Hobbits.Mb,
@@ -45,12 +41,14 @@
                    Data.Binding.Hobbits.QQ,
                    Data.Binding.Hobbits.Liftable,
 
-                   Data.Binding.Hobbits.Internal,
                    Data.Binding.Hobbits.PatternParser,
-                   Data.Binding.Hobbits.NuElim,
+                   Data.Binding.Hobbits.NuMatching,
 
                    Data.Binding.Hobbits.Examples.LambdaLifting,
                    Data.Binding.Hobbits.Examples.LambdaLifting.Terms,
                    Data.Binding.Hobbits.Examples.LambdaLifting.Examples
 
-  Other-Modules: Data.Binding.Hobbits.InternalUtilities
+  Other-Modules: Data.Binding.Hobbits.Internal.Utilities,
+                   Data.Binding.Hobbits.Internal.Name
+                   Data.Binding.Hobbits.Internal.Mb
+                   Data.Binding.Hobbits.Internal.Closed
diff --git a/output b/output
deleted file mode 100644
--- a/output
+++ /dev/null
@@ -1,20 +0,0 @@
-Glasgow Haskell Compiler, Version 7.6.3, stage 2 booted by GHC version 7.4.2
-Using binary package database: /Library/Frameworks/GHC.framework/Versions/7.6.3-x86_64/usr/lib/ghc-7.6.3/package.conf.d/package.cache
-Using binary package database: /Users/eddy/.ghc/x86_64-darwin-7.6.3/package.conf.d/package.cache
-hiding package Cabal-1.16.0 to avoid conflict with later version Cabal-1.18.1.2
-wired-in package ghc-prim mapped to ghc-prim-0.3.0.0-d5221a8c8a269b66ab9a07bdc23317dd
-wired-in package integer-gmp mapped to integer-gmp-0.5.0.0-2f15426f5b53fe4c6490832f9b20d8d7
-wired-in package base mapped to base-4.6.0.1-6c351d70a24d3e96f315cba68f3acf57
-wired-in package rts mapped to builtin_rts
-wired-in package template-haskell mapped to template-haskell-2.8.0.0-c2c1b21dbbb37ace4b7dc26c966ec664
-wired-in package dph-seq not found.
-wired-in package dph-par not found.
-Hsc static flags: -static
-Created temporary directory: /var/folders/st/cjmsx__d5f17m4_1qn0dxkpr0000gn/T/ghc36361_0
-*** C pre-processor:
-'/usr/bin/clang-wrapper' '-E' '-undef' '-traditional' '-m64' '-fno-stack-protector' '-m64' '-I' '/Library/Frameworks/GHC.framework/Versions/7.6.3-x86_64/usr/lib/ghc-7.6.3/base-4.6.0.1/include' '-I' '/Library/Frameworks/GHC.framework/Versions/7.6.3-x86_64/usr/lib/ghc-7.6.3/include' '-D__GLASGOW_HASKELL__=706' '-Ddarwin_BUILD_OS=1' '-Dx86_64_BUILD_ARCH=1' '-Ddarwin_HOST_OS=1' '-Dx86_64_HOST_ARCH=1' '-U __PIC__' '-D__PIC__' '-include' 'dist/build/autogen/cabal_macros.h' '-D__GLASGOW_HASKELL__=706' '-Ddarwin_BUILD_OS=1' '-Dx86_64_BUILD_ARCH=1' '-Ddarwin_HOST_OS=1' '-Dx86_64_HOST_ARCH=1' '-x' 'c' 'Data/Type/List.hs' '-o' '/var/folders/st/cjmsx__d5f17m4_1qn0dxkpr0000gn/T/ghc36361_0/ghc36361_0.hscpp'
-*** Copying `/var/folders/st/cjmsx__d5f17m4_1qn0dxkpr0000gn/T/ghc36361_0/ghc36361_0.hscpp' to `dist/build/tmp-36333/Data/Type/List.hs':
-*** Deleting temp files:
-Deleting: /var/folders/st/cjmsx__d5f17m4_1qn0dxkpr0000gn/T/ghc36361_0/ghc36361_0.hscpp
-*** Deleting temp dirs:
-Deleting: /var/folders/st/cjmsx__d5f17m4_1qn0dxkpr0000gn/T/ghc36361_0