diff --git a/CHANGES b/CHANGES
--- a/CHANGES
+++ b/CHANGES
@@ -28,3 +28,12 @@
     Thanks to Sean Leather for the report.
 
   * Clean up some compiler warnings.
+
+Version 0.2.6: 24 August 2011
+
+  * New permutation- and set-binding functions, for creating binders
+    which don't care about the order of multiple bound names, and/or
+    about unused bound names.
+
+  * Bump RepLib dependency to 0.5, which now has support for GADTs
+    without existential type variables.
diff --git a/Unbound/LocallyNameless.hs b/Unbound/LocallyNameless.hs
--- a/Unbound/LocallyNameless.hs
+++ b/Unbound/LocallyNameless.hs
@@ -100,9 +100,13 @@
 
     Bind,
 
-    -- *** Bind constructor
+    -- *** Bind constructors
     bind,
+    permbind,
+    setbind,
+    setbindAny,
 
+
     -- *** Bind destructors
 
     -- | Directly pattern-matching on 'Bind' values is not allowed,
@@ -250,7 +254,7 @@
     -- | These type representation objects are exported so they can be
     --   referenced by auto-generated code.  Please pretend they do not
     --   exist.
-    rName, rBind, rRebind, rEmbed, rRec, rShift
+    rName, rGenBind, rRebind, rEmbed, rRec, rShift
 ) where
 
 import Unbound.LocallyNameless.Name
diff --git a/Unbound/LocallyNameless/Alpha.hs b/Unbound/LocallyNameless/Alpha.hs
--- a/Unbound/LocallyNameless/Alpha.hs
+++ b/Unbound/LocallyNameless/Alpha.hs
@@ -666,7 +666,7 @@
 
   nthpatrec = nthName
 
-instance (Alpha p, Alpha t) => Alpha (Bind p t) where
+instance (Rep order, Rep card, Alpha p, Alpha t) => Alpha (GenBind order card p t) where
     isPat _ = Nothing
     isTerm (B p t) = isJust (isPat p) && isTerm t
 
diff --git a/Unbound/LocallyNameless/Ops.hs b/Unbound/LocallyNameless/Ops.hs
--- a/Unbound/LocallyNameless/Ops.hs
+++ b/Unbound/LocallyNameless/Ops.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE TypeSynonymInstances #-}
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 ----------------------------------------------------------------------
 -- |
@@ -19,6 +20,10 @@
 import Unbound.Util
 import Unbound.PermM
 
+import Data.Maybe (catMaybes)
+import Data.List  (sortBy)
+import Data.Ord   (comparing)
+
 import Control.Monad (liftM)
 import qualified Text.Read as R
 
@@ -35,7 +40,7 @@
 
 -- | A destructor for binders that does /not/ guarantee fresh
 --   names for the binders.
-unsafeUnbind :: (Alpha a, Alpha b) => Bind a b -> (a,b)
+unsafeUnbind :: (Alpha a, Alpha b) => GenBind order card a b -> (a,b)
 unsafeUnbind (B a b) = (a, openT a b)
 
 instance (Alpha a, Alpha b, Read a, Read b) => Read (Bind a b) where
@@ -50,6 +55,80 @@
          readListPrec = R.readListPrecDefault
 
 ----------------------------------------------------------
+-- Set Binding operations
+----------------------------------------------------------
+
+permCloseAny :: (Alpha t) => [AnyName] -> t -> ([AnyName],t)
+permCloseAny ns t = (ns', closeT ns' t) where
+    -- find where the names occur in the body of the term
+    ns' = map fst . sortBy (comparing snd) 
+        . catMaybes 
+        . map (strength . (\n -> (n, findpat t n))) 
+        $ ns
+
+strength :: Functor f => (a, f b) -> f (a, b)
+strength (a, fb) = fmap ((,) a) fb
+
+-- Given a list of names and a term, close the term with those names
+-- where the indices of the bound variables occur in sequential order
+-- and return the equivalent ordering of the names, dropping those
+-- that do not occur in the term at all
+-- For example:
+--    permClose [b,c]    (b,c)   =  ([b,c], (0,1))    -- standard close
+--    permClose [b,c]    (c,b)   =  ([c,b], (0,1))    -- vars reordered
+--    permClose [a,b,c]  (c,b)   =  ([c,b], (0,1))    -- var dropped
+--    permClose [a,b,c]  (c,b,c) =  ([c,b], (0,1,0))  -- additional occurrence ok
+
+permClose :: (Alpha a, Alpha t) => [Name a] -> t -> ([Name a],t)
+permClose ns t = (ns', closeT ns' t) where
+    ns' = map fst . sortBy (comparing snd) 
+        . catMaybes 
+        . map (strength . (\n -> (n, findpat t (AnyName n))))
+        $ ns
+
+-- | Bind the pattern in the term \"up to permutation\" of bound variables.
+--   For example, the following 4 terms are /all/ alpha-equivalent:
+--
+--   > permbind [a,b] (a,b)
+--   > permbind [a,b] (b,a)
+--   > permbind [b,a] (a,b)
+--   > permbind [b,a] (b,a)
+--
+--   Note that none of these terms is equivalent to a term with a
+--   redundant pattern such as
+--
+--   > permbind [a,b,c] (a,b)
+--
+--   For binding constructors which /do/ render these equivalent,
+--   see 'setbind' and 'setbindAny'.
+permbind :: (Alpha p, Alpha t) => p -> t -> SetBind p t
+permbind p t = B p (snd $ permCloseAny (bindersAny p) t)
+
+-- | Bind the list of names in the term up to permutation and dropping
+--   of unused variables.
+--
+--   For example, the following 5 terms are /all/ alpha-equivalent:
+--
+--   > setbind [a,b] (a,b)
+--   > setbind [a,b] (b,a)
+--   > setbind [b,a] (a,b)
+--   > setbind [b,a] (b,a)
+--   > setbind [a,b,c] (a,b)
+--
+--   There is also a variant, 'setbindAny', which ignores name sorts.
+setbind ::(Alpha a, Alpha t) => [Name a] -> t -> SetPlusBind [Name a] t
+setbind p t = B ns t' where
+         (ns, t') = permClose (binders p) t
+
+-- | Bind the list of (any-sorted) names in the term up to permutation
+--   and dropping of unused variables.  See 'setbind'.
+setbindAny :: (Alpha t) => [AnyName] -> t -> SetPlusBind [AnyName] t
+setbindAny p t = B ns t' where
+         (ns, t') = permCloseAny (bindersAny p) t
+
+
+
+----------------------------------------------------------
 -- Rebinding operations
 ----------------------------------------------------------
 
@@ -210,7 +289,7 @@
 --   bindings. It ensures that the names in the binding are globally
 --   fresh, using a monad which is an instance of the 'Fresh' type
 --   class.
-unbind :: (Fresh m, Alpha p, Alpha t) => Bind p t -> m (p,t)
+unbind :: (Fresh m, Alpha p, Alpha t) => GenBind order card p t -> m (p,t)
 unbind (B p t) = do
       (p', _) <- freshen p
       return (p', openT p' t)
@@ -221,7 +300,7 @@
 --   @Nothing@.  Otherwise, return the renamed patterns and the
 --   associated terms.
 unbind2 :: (Fresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2) =>
-            Bind p1 t1 -> Bind p2 t2 -> m (Maybe (p1,t1,p2,t2))
+            GenBind order card p1 t1 -> GenBind order card p2 t2 -> m (Maybe (p1,t1,p2,t2))
 unbind2 (B p1 t1) (B p2 t2) = do
       case mkPerm (fvAny p2) (fvAny p1) of
          Just pm -> do
@@ -234,7 +313,7 @@
 --   binders have the same number of binding variables.  See the
 --   documentation for 'unbind2' for more details.
 unbind3 :: (Fresh m, Alpha p1, Alpha p2, Alpha p3, Alpha t1, Alpha t2, Alpha t3) =>
-            Bind p1 t1 -> Bind p2 t2 -> Bind p3 t3 ->  m (Maybe (p1,t1,p2,t2,p3,t3))
+            GenBind order card p1 t1 -> GenBind order card p2 t2 -> GenBind order card p3 t3 ->  m (Maybe (p1,t1,p2,t2,p3,t3))
 unbind3 (B p1 t1) (B p2 t2) (B p3 t3) = do
       case ( mkPerm (fvAny p2) (fvAny p1)
            , mkPerm (fvAny p3) (fvAny p1) ) of
@@ -253,7 +332,7 @@
 --
 --   For more information, see the documentation for the 'LFresh' type
 --   class.
-lunbind :: (LFresh m, Alpha p, Alpha t) => Bind p t -> ((p, t) -> m c) -> m c
+lunbind :: (LFresh m, Alpha p, Alpha t) => GenBind order card p t -> ((p, t) -> m c) -> m c
 lunbind (B p t) g =
   lfreshen p (\x _ -> g (x, openT x t))
 
@@ -262,7 +341,7 @@
 --   patterns have the same number of binding variables.  See the
 --   documentation for 'unbind2' and 'lunbind' for more details.
 lunbind2  :: (LFresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2) =>
-            Bind p1 t1 -> Bind p2 t2 -> (Maybe (p1,t1,p2,t2) -> m r) -> m r
+            GenBind order card p1 t1 -> GenBind order card p2 t2 -> (Maybe (p1,t1,p2,t2) -> m r) -> m r
 lunbind2 (B p1 t1) (B p2 t2) g =
   case mkPerm (fvAny p2) (fvAny p1) of
     Just pm1 ->
@@ -274,7 +353,7 @@
 --   the binders have the same number of binding variables.  See the
 --   documentation for 'unbind2' and 'lunbind' for more details.
 lunbind3 :: (LFresh m, Alpha p1, Alpha p2, Alpha p3, Alpha t1, Alpha t2, Alpha t3) =>
-            Bind p1 t1 -> Bind p2 t2 -> Bind p3 t3 ->
+            GenBind order card p1 t1 -> GenBind order card p2 t2 -> GenBind order card p3 t3 ->
             (Maybe (p1,t1,p2,t2,p3,t3) -> m r) ->
             m r
 lunbind3 (B p1 t1) (B p2 t2) (B p3 t3) g =
diff --git a/Unbound/LocallyNameless/Subst.hs b/Unbound/LocallyNameless/Subst.hs
--- a/Unbound/LocallyNameless/Subst.hs
+++ b/Unbound/LocallyNameless/Subst.hs
@@ -117,8 +117,8 @@
 instance (Subst c a) => Subst c (Maybe a)
 instance (Subst c a, Subst c b) => Subst c (Either a b)
 
-instance (Subst c b, Subst c a, Alpha a,Alpha b) =>
-    Subst c (Bind a b)
+instance (Rep order, Rep card, Subst c b, Subst c a, Alpha a,Alpha b) =>
+    Subst c (GenBind order card a b)
 instance (Subst c b, Subst c a, Alpha a, Alpha b) =>
     Subst c (Rebind a b)
 
diff --git a/Unbound/LocallyNameless/Types.hs b/Unbound/LocallyNameless/Types.hs
--- a/Unbound/LocallyNameless/Types.hs
+++ b/Unbound/LocallyNameless/Types.hs
@@ -3,6 +3,7 @@
            , FlexibleInstances
            , FlexibleContexts
            , MultiParamTypeClasses
+           , EmptyDataDecls
   #-}
 
 ----------------------------------------------------------------------
@@ -18,7 +19,7 @@
 ----------------------------------------------------------------------
 
 module Unbound.LocallyNameless.Types
-       ( Bind(..)
+       ( GenBind(..), Bind, SetBind, SetPlusBind
        , Rebind(..)
        , Rec(..)
        , TRec(..)
@@ -32,7 +33,7 @@
        --   referenced by auto-generated code.  Please pretend they do not
        --   exist.
 
-       , rBind, rRebind, rEmbed, rRec, rShift
+       , rGenBind, rRebind, rEmbed, rRec, rShift
        ) where
 
 import Generics.RepLib
@@ -42,23 +43,32 @@
 -- Basic types
 ------------------------------------------------------------
 
+data RelaxedOrder
+data StrictOrder
+
+data RelaxedCard
+data StrictCard
+
 -- Bind
 --------------------------------------------------
 
+-- XXX update documentation
 -- | The most fundamental combinator for expressing binding structure
 --   is 'Bind'.  The /term type/ @Bind p t@ represents a pattern @p@
 --   paired with a term @t@, where names in @p@ are bound within @t@.
 --
 --   Like 'Name', 'Bind' is also abstract. You can create bindings
 --   using 'bind' and take them apart with 'unbind' and friends.
-data Bind p t = B p t
+data GenBind order card p t = B p t
 
-instance (Show a, Show b) => Show (Bind a b) where
+type Bind p t        = GenBind StrictOrder StrictCard p t
+type SetBind p t     = GenBind RelaxedOrder StrictCard p t
+type SetPlusBind p t = GenBind RelaxedOrder RelaxedCard p t
+
+instance (Show a, Show b) => Show (GenBind order card a b) where
   showsPrec p (B a b) = showParen (p>0)
       (showString "<" . showsPrec p a . showString "> " . showsPrec 0 b)
 
--- XXX todo: make sure everything has write Read and Eq instances?
-
 -- Rebind
 --------------------------------------------------
 
@@ -133,5 +143,7 @@
 
 -- Pay no attention...
 
-$(derive [''Bind, ''Embed, ''Rebind, ''Rec, ''Shift])
+$(derive [''GenBind, ''Embed, ''Rebind, ''Rec, ''Shift])
+
+$(derive [''RelaxedOrder, ''StrictOrder, ''RelaxedCard, ''StrictCard])
 
diff --git a/Unbound/PermM.hs b/Unbound/PermM.hs
--- a/Unbound/PermM.hs
+++ b/Unbound/PermM.hs
@@ -17,7 +17,6 @@
 import Data.Monoid
 import Data.List
 import Data.Map (Map)
-import Data.Function (on)
 import qualified Data.Map as M
 import qualified Data.Set as S
 import Control.Arrow ((&&&))
diff --git a/examples/Set.hs b/examples/Set.hs
new file mode 100644
--- /dev/null
+++ b/examples/Set.hs
@@ -0,0 +1,67 @@
+{-# LANGUAGE TemplateHaskell, UndecidableInstances, ExistentialQuantification,
+    TypeOperators, GADTs, TypeSynonymInstances, FlexibleInstances,
+    ScopedTypeVariables, MultiParamTypeClasses, StandaloneDeriving
+ #-}
+
+module Set where
+
+import Generics.RepLib
+import Unbound.LocallyNameless
+import Data.List
+import Data.Set
+
+data Ty = All (Bind [Name Ty] Ty)
+        | Var (Name Ty)
+        | Arr Ty Ty deriving Show
+
+$(derive [''Ty])
+
+$(derive_abstract [''Set])
+
+instance Alpha Ty
+
+a, b, c :: Name Ty
+a = s2n "a"
+b = s2n "b"
+c = s2n "c"
+
+sall :: [Name Ty] -> Ty -> Ty
+sall ns t = All (setbind ns t)
+
+s1 = sall [a, b] (Arr (Var a) (Var b))
+s2 = sall [a, b] (Arr (Var b) (Var a))
+s3 = sall [b, a] (Arr (Var a) (Var b))
+s4 = sall [b, a] (Arr (Var b) (Var a))
+s5 = sall [b, a, c] (Arr (Var b) (Var a))
+s6 = sall [a, c] (Arr (Var a) (Var c))
+
+pall :: [Name Ty] -> Ty -> Ty
+pall ns t = All (permbind ns t)
+
+p1 = pall [a, b] (Arr (Var a) (Var b))
+p2 = pall [a, b] (Arr (Var b) (Var a))
+p3 = pall [b, a] (Arr (Var a) (Var b))
+p4 = pall [b, a] (Arr (Var b) (Var a))
+p5 = pall [b, a, c] (Arr (Var b) (Var a))
+p6 = pall [a, c] (Arr (Var a) (Var c))
+
+
+
+assert :: String -> Bool -> IO ()
+assert s True  = return ()
+assert s False = print ("Assertion " ++ s ++ " failed")
+
+main :: IO ()
+main = do
+  assert "s1" $ s1 `aeq` s2
+  assert "s2" $ s1 `aeq` s3
+  assert "s3" $ s1 `aeq` s4
+  assert "s4" $ s1 `aeq` s5
+  assert "s5" $ s1 `aeq` s6
+
+  assert "a11" $ p1 `aeq` p2
+  assert "a12" $ p1 `aeq` p3
+  assert "a13" $ p1 `aeq` p4
+  assert "a14" $ not (p1 `aeq` p5)
+  assert "a15" $ p1 `aeq` p6
+
diff --git a/examples/TaggedTerm.hs b/examples/TaggedTerm.hs
new file mode 100644
--- /dev/null
+++ b/examples/TaggedTerm.hs
@@ -0,0 +1,59 @@
+{-# LANGUAGE TemplateHaskell
+           , UndecidableInstances
+           , TypeOperators
+           , GADTs
+           , FlexibleInstances
+           , ScopedTypeVariables
+           , MultiParamTypeClasses
+           , KindSignatures
+           , RankNTypes
+           , StandaloneDeriving
+           , OverlappingInstances
+ #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  TaggedTerm
+-- Copyright   :  (c) the Unbound team (see LICENSE)
+-- License     :  BSD-like (see LICENSE)
+--
+-- Maintainer  :  byorgey@cis.upenn.edu
+-- Stability   :  experimental
+-- Portability :  non-portable
+-----------------------------------------------------------------------------
+
+module TaggedTerm where
+
+import Unbound.LocallyNameless hiding (Con)
+
+data Term
+data Pattern
+
+data Expr :: * -> * where
+         -- Note: be very careful here!  Name (Expr a) -> Expr a does
+         -- not work since the names in patterns will not get
+         -- connected up with names in terms.
+  Var :: Name (Expr Term) -> Expr a
+  App :: Expr a ->  Expr a -> Expr a
+  Lam :: Bind (Expr Pattern) (Expr Term) -> Expr Term
+  Con :: String -> [Expr a] -> Expr a
+
+deriving instance Show (Expr a)
+
+$(derive [''Term, ''Pattern, ''Expr])
+
+instance (Rep t) => Alpha (Expr t)
+
+instance Subst (Expr Term) (Expr Term) where
+  isvar (Var x) = Just (SubstName x)
+  isvar _       = Nothing
+
+instance Subst (Expr Term) (Expr Pattern)
+
+test1 :: Expr Term
+test1 = Lam (bind (Con "Pair" [Var $ s2n "y", Var $ s2n "z"]) (Con "Pair" [Var (s2n "y"), Var (s2n "x")]))
+
+test2 :: Expr Term
+test2 = subst (s2n "y") (Con "Unit" [] :: Expr Term) test1
+
+test3 :: Expr Term
+test3 = subst (s2n "x") (Con "Unit" [] :: Expr Term) test1
diff --git a/examples/Vec.hs b/examples/Vec.hs
new file mode 100644
--- /dev/null
+++ b/examples/Vec.hs
@@ -0,0 +1,54 @@
+{-# LANGUAGE TemplateHaskell
+           , UndecidableInstances
+           , TypeOperators
+           , GADTs
+           , FlexibleInstances
+           , ScopedTypeVariables
+           , MultiParamTypeClasses
+           , KindSignatures
+           , RankNTypes
+           , StandaloneDeriving
+           , OverlappingInstances
+ #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Vec
+-- Copyright   :  (c) the Unbound team (see LICENSE)
+-- License     :  BSD-like (see LICENSE)
+--
+-- Maintainer  :  byorgey@cis.upenn.edu
+-- Stability   :  experimental
+-- Portability :  non-portable
+-----------------------------------------------------------------------------
+
+module Vec where
+
+import Unbound.LocallyNameless hiding (Nil)
+
+data Z
+data S n
+
+data Vec :: * -> * -> * where
+  Nil   :: Vec Z a
+  Cons  :: a -> Vec n a -> Vec (S n) a
+
+deriving instance Show a => Show (Vec n a)
+
+data Term = Var (Name Term) 
+          | Lit (Vec (S (S Z)) Int) 
+          | Pair Term Term
+  deriving Show
+
+$(derive [''Z, ''S, ''Vec, ''Term])
+
+instance (Alpha a, Rep n) => Alpha (Vec n a)
+instance Alpha Term
+
+instance Subst Term Term where
+  isvar (Var x) = Just (SubstName x)
+  isvar _       = Nothing
+
+instance (Rep n, Rep a) => Subst Term (Vec n a)
+
+t :: Term
+t = Pair (Var (s2n "x")) (Lit (Cons 1 (Cons 2 Nil)))
diff --git a/unbound.cabal b/unbound.cabal
--- a/unbound.cabal
+++ b/unbound.cabal
@@ -1,5 +1,5 @@
 name:           unbound
-version:        0.2.5
+version:        0.3
 license:        BSD3
 license-file:   LICENSE
 build-type:     Simple
@@ -30,7 +30,7 @@
 
 Library
   build-depends: base >= 4.3 && < 5,
-                 RepLib >= 0.4.0,
+                 RepLib >= 0.5,
                  mtl >= 2.0 && < 2.1, transformers >= 0.2.2.0 && < 0.2.3,
                  containers >= 0.3 && < 0.5
   exposed-modules: