diff --git a/bound.cabal b/bound.cabal
--- a/bound.cabal
+++ b/bound.cabal
@@ -1,6 +1,6 @@
 name:          bound
 category:      Language, Compilers/Interpreters
-version:       0.1
+version:       0.1.1
 license:       BSD3
 cabal-version: >= 1.6
 license-file:  LICENSE
@@ -14,7 +14,7 @@
 description:   Combinators for manipulating locally-nameless generalized de Bruijn terms
 
 build-type:    Simple
-extra-source-files: .travis.yml examples/Simple.hs examples/Exp.hs
+extra-source-files: .travis.yml examples/Simple.hs examples/Deriving.hs examples/Overkill.hs
 
 source-repository head
   type: git
diff --git a/examples/Deriving.hs b/examples/Deriving.hs
new file mode 100644
--- /dev/null
+++ b/examples/Deriving.hs
@@ -0,0 +1,93 @@
+{-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable #-}
+module Exp where
+
+import Data.List
+import Data.Foldable
+import Data.Traversable
+import Control.Monad
+import Control.Applicative
+import Prelude.Extras
+import Bound
+
+infixl 9 :@
+
+data Exp a
+  = Var a
+  | Exp a :@ Exp a
+  | Lam {-# UNPACK #-} !Int (Pat Exp a) (Scope Int Exp a)
+  | Let {-# UNPACK #-} !Int [Scope Int Exp a] (Scope Int Exp a)
+  | Case (Exp a) [Alt Exp a]
+  deriving (Eq,Ord,Show,Read,Functor,Foldable,Traversable)
+
+instance Applicative Exp where
+  pure = Var
+  (<*>) = ap
+
+instance Monad Exp where
+  return          = Var
+  Var a      >>= f = f a
+  (x :@ y)   >>= f = (x >>= f) :@ (y >>= f)
+  Lam n p e  >>= f = Lam n (p >>>= f) (e >>>= f)
+  Let n bs e >>= f = Let n (map (>>>= f) bs) (e >>>= f)
+  Case e as  >>= f = Case (e >>= f) (map (>>>= f) as)
+
+instance Eq1   Exp where (==#) = (==)
+instance Ord1  Exp where compare1 = compare
+instance Show1 Exp where showsPrec1 = showsPrec
+instance Read1 Exp where readsPrec1 = readsPrec
+
+data Pat f a
+  = VarP
+  | WildP
+  | AsP (Pat f a)
+  | ConP String [Pat f a]
+  | ViewP (f a) (Pat f a)
+  deriving (Eq,Ord,Show,Read,Functor,Foldable,Traversable)
+
+instance Bound Pat where
+  VarP      >>>= _ = VarP
+  WildP     >>>= _ = WildP
+  AsP p     >>>= f = AsP (p >>>= f)
+  ConP g ps >>>= f = ConP g (map (>>>= f) ps)
+  ViewP e p >>>= f = ViewP (e >>= f) (p >>>= f)
+
+data Alt f a = Alt {-# UNPACK #-} !Int (Pat f a) (Scope Int f a)
+  deriving (Eq,Ord,Show,Read,Functor,Foldable,Traversable)
+
+instance Bound Alt where
+  Alt n p b >>>= f = Alt n (p >>>= f) (b >>>= f)
+
+-- ** smart patterns
+
+data P a = P { pattern :: Pat Exp a, bindings :: [a] }
+
+varp :: a -> P a
+varp a = P VarP [a]
+
+wildp :: P a
+wildp = P WildP []
+
+asp :: a -> P a -> P a
+asp a (P p as) = P (AsP p) (a:as)
+
+conp :: String -> [P a] -> P a
+conp g ps = P (ConP g (map pattern ps)) (ps >>= bindings)
+
+-- | smart lam constructor
+lam :: Eq a => P a -> Exp a -> Exp a
+lam (P p as) t = Lam (length as) p (abstract (`elemIndex` as) t)
+
+-- | smart let constructor
+let_ :: Eq a => [(a, Exp a)] -> Exp a -> Exp a
+let_ bs b = Let (length bs) (map (abstr . snd) bs) (abstr b)
+  where vs  = map fst bs
+        abstr = abstract (`elemIndex` vs)
+
+-- | smart alt constructor
+alt :: Eq a => P a -> Exp a -> Alt Exp a
+alt (P p as) t = Alt (length as) p (abstract (`elemIndex` as) t)
+
+-- ghci> let_ [("x",Var "y"),("y",Var "x" :@ Var "y")] $ lam (varp "z") (Var "z" :@ Var "y")
+-- ghci> lam (varp "x") (Var "x")
+-- ghci> lam (conp "Hello" [varp "x", wildp])) (Var "y")
+-- ghci> lam (varp "x") $ Case (Var "x") [alt (conp "Hello" [varp "z",wildp]) (Var "x"), alt (varp "y") (Var "y")]
diff --git a/examples/Exp.hs b/examples/Exp.hs
deleted file mode 100644
--- a/examples/Exp.hs
+++ /dev/null
@@ -1,308 +0,0 @@
-{-# LANGUAGE StandaloneDeriving #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE UndecidableInstances #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE KindSignatures #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE ExistentialQuantification #-}
-{-# LANGUAGE TypeOperators #-}
-module Exp where
-
-
-import Data.Vector as Vector hiding ((++), map)
-import Data.List as List
-import Data.Foldable
-import Data.Traversable
-import Data.Monoid (Monoid(..))
-import Control.Monad
-import Control.Monad.Trans.Class
-import Control.Applicative
-import Prelude hiding (foldr)
-import Prelude.Extras
-import GHC.Prim (Constraint(..))
-import Unsafe.Coerce
-import Bound
-
--- ghci> let_ [("x",Var "y"),("y",Var "x" :@ Var "y")] $ lam (varp "z") (Var "z" :@ Var "y")
--- Let (fromList [Scope (Var (B 1)),Scope (Var (B 0) :@ Var (B 1))]) (Scope (Lam VarP (Scope (Var (B V) :@ Var (F (Var (B 1)))))))
---
--- ghc> lam (varp "x") (Var "x")
--- ghc> lam (conp "Hello" [varp "x", wildp])) (Var "y")
-
-infixl 9 :@
-infixr 5 :>
-
--- little orphan instances
-instance Show1 Vector where showsPrec1 = showsPrec
-instance Eq1 Vector where (==#) = (==)
-
-data Exp a
-  = Var a
-  | Exp a :@ Exp a
-  | forall (b :: Index). Lam (Pat b Exp a) (Scope (Path b) Exp a)
-  | Let (Vector (Scope Int Exp a)) (Scope Int Exp a)
-  -- | Case (Exp a) [Alt Exp a]
-
-data Alt f a = forall b. Alt (Pat b f a) (Scope (Path b) Exp a)
-
-data Index = VarI | WildI | AsI Index | ConI [Index]
-
-data Pat :: Index -> (* -> *) -> * -> * where
-  VarP  ::                             Pat VarI f a
-  WildP ::                             Pat WildI f a
-  AsP   :: Pat i f a                -> Pat (AsI i) f a
-  ConP  :: String    -> Pats bs f a -> Pat (ConI bs) f a
-  ViewP :: f a       -> Pat b f a   -> Pat b f a -- TODO: allow references to earlier variables
-
-data Pats :: [Index] -> (* -> *) -> * -> * where
-  NilP  :: Pats '[] f a
-  (:>) :: Pat b f a -> Pats bs f a -> Pats (b ': bs) f a
-
-data Path :: Index -> * where
-  V :: Path VarI
-  L :: Path (AsI a)
-  R :: Path a -> Path (AsI a)
-  C :: MPath as -> Path (ConI as)
-
-data MPath :: [Index] -> * where
-  H :: Path a   -> MPath (a ':as)
-  T :: MPath as -> MPath (a ':as)
-
-instance Functor Exp where
-  fmap = fmapDefault
-
-instance Foldable Exp where
-  foldMap = foldMapDefault
-
-instance Applicative Exp where
-  pure = Var
-  (<*>) = ap
-
-instance Traversable Exp where
-  traverse f (Var a)    = Var <$> f a
-  traverse f (x :@ y)   = (:@) <$> traverse f x <*> traverse f y
-  traverse f (Lam p e)  = Lam <$> traverse f p <*> traverse f e
-  traverse f (Let bs e) = Let <$> traverse (traverse f) bs <*> traverse f e
-
-instance Monad Exp where
-  return         = Var
-  Var a    >>= f = f a
-  (x :@ y) >>= f = (x >>= f) :@ (y >>= f)
-  Lam p e  >>= f = Lam (p >>>= f) (e >>>= f)
-  Let bs e >>= f = Let (fmap (>>>= f) bs) (e >>>= f)
- -- Case e as >>= f = Case (e >>= f) (fmap (>>>= f) as)
-
-instance Eq a => Eq (Exp a) where (==) = (==#)
-instance Eq1 Exp where
-  Var a     ==# Var b     = a == b
-  (a :@ b)  ==# (c :@ d)  = a ==# c && b ==# d
-  Lam ps a  ==# Lam qs b  = eqPat ps qs && a ==# unsafeCoerce b -- eqPat proves equal shape
-  Let as a  ==# Let bs b  = as == bs && a ==# b
- -- Case e as ==# Case f bs = e ==# f && as == bs
-  _         ==# _         = False
-
-instance Show a => Show (Exp a) where showsPrec = showsPrec1
-instance Show1 Exp where
-  showsPrec1 d (Var a)    = showParen (d > 10) $ showString "Var " . showsPrec 11 a
-  showsPrec1 d (a :@ b)   = showParen (d > 9) $ showsPrec1 9 a . showString " :@ " . showsPrec1 10 b
-  showsPrec1 d (Lam ps b) = showParen (d > 10) $ showString "Lam " . showsPrec1 11 ps . showChar ' ' . showsPrec1 11 b
-  showsPrec1 d (Let bs b) = showParen (d > 10) $ showString "Let " . showsPrec1 11 bs . showChar ' ' . showsPrec1 11 b
-
-{-
-instance Eq1 f => Eq1 (Alt f) where
-  Alt p s ==# Alt q t = eqPat p q && s == unsafeCoerce t
-
-instance (Eq1 f, Eq a) => Eq (Alt f) where (==) = (==#)
-
-instance Show1 f => Show1 (Alt f) where
-  showsPrec d (Alt p s) = showsPrec d (Alt p s)
--}
-
-
--- * smart lam
-
--- ** smart patterns
-
-data P a = forall b. P (Pat b Exp a) [a] (a -> Maybe (Path b))
-
-varp :: Eq a => a -> P a
-varp a = P VarP [a] (\v -> if a == v then Just V else Nothing)
-
-wildp :: P a
-wildp = P WildP [] (const Nothing)
-
-asp :: Eq a => a -> P a -> P a
-asp a (P p as f) = P (AsP p) (a:as) $ \v -> case f v of
-  Just b              -> Just (R b)
-  Nothing | a == v    -> Just L
-          | otherwise -> Nothing
-
-data Ps a = forall bs. Ps (Pats bs Exp a) [a] (a -> Maybe (MPath bs))
-
-conp :: String -> [P a] -> P a
-conp g ps = case go ps of
-  Ps qs as f -> P (ConP g qs) as (fmap C . f)
-  where
-    go :: [P a] -> Ps a
-    go [] = Ps NilP [] (const Nothing)
-    go (P p as f : xs) = case go xs of
-      Ps ps ass g -> Ps (p :> ps) (as ++ ass) $ \v ->
-        T <$> g v <|> H <$> f v
-
--- * smart lam
-lam :: P a -> Exp a -> Exp a
-lam (P p _ f) t = Lam p (abstract f t)
-
--- * smart let
-let_ :: Eq a => [(a, Exp a)] -> Exp a -> Exp a
-let_ bs b = Let (Vector.fromList $ map (abstr . snd) bs) (abstr b)
-  where vs  = map fst bs
-        abstr = abstract (`List.elemIndex` vs)
-
--- * Pat
-
--- ** A Kind of Shape
-
-eqPat :: (Eq1 f, Eq a) => Pat b f a -> Pat b' f a -> Bool
-eqPat VarP        VarP        = True
-eqPat WildP       WildP       = True
-eqPat (AsP p)     (AsP q)     = eqPat p q
-eqPat (ConP g ps) (ConP h qs) = g == h  && eqPats ps qs
-eqPat (ViewP e p) (ViewP f q) = e ==# f && eqPat p q
-
-instance Eq1 f   => Eq1 (Pat b f)        where (==#) = eqPat
-instance (Eq1 f, Eq a) => Eq (Pat b f a) where (==) = eqPat
-
-instance Show1 f => Show1 (Pat b f) where showsPrec1 = showsPrec
-instance (Show1 f, Show a) => Show (Pat b f a) where
-  showsPrec _ VarP        = showString "VarP"
-  showsPrec _ WildP       = showString "WildP"
-  showsPrec d (AsP p)     = showParen (d > 10) $ showString "AsP " . showsPrec 11 p
-  showsPrec d (ConP g ps) = showParen (d > 10) $ showString "ConP " . showsPrec 11 g . showChar ' ' . showsPrec 11 ps
-  showsPrec d (ViewP e p) = showParen (d > 10) $ showString "ViewP " . showsPrec1 11 e . showChar ' ' . showsPrec 11 p
-
-instance Functor f => Functor (Pat b f) where
-  fmap _ VarP = VarP
-  fmap _ WildP = WildP
-  fmap f (AsP p) = AsP (fmap f p)
-  fmap f (ConP g ps) = ConP g (fmap f ps)
-  fmap f (ViewP e p) = ViewP (fmap f e) (fmap f p)
-
-instance Foldable f => Foldable (Pat b f) where
-  foldMap f (AsP p)     = foldMap f p
-  foldMap f (ConP g ps) = foldMap f ps
-  foldMap f (ViewP e p) = foldMap f e `mappend` foldMap f p
-  foldMap _ _           = mempty
-
-instance Traversable f => Traversable (Pat b f) where
-  traverse _ VarP = pure VarP
-  traverse _ WildP = pure WildP
-  traverse f (AsP p) = AsP <$> traverse f p
-  traverse f (ConP g ps) = ConP g <$> traverse f ps
-  traverse f (ViewP e p) = ViewP <$> traverse f e <*> traverse f p
-
-instance Bound (Pat b) where
-  VarP      >>>= _ = VarP
-  WildP     >>>= _ = WildP
-  AsP p     >>>= f = AsP (p >>>= f)
-  ConP g ps >>>= f = ConP g (ps >>>= f)
-  ViewP e p >>>= f = ViewP (e >>= f) (p >>>= f)
-
--- ** Pats
-
-
-eqPats :: (Eq1 f, Eq a) => Pats bs f a -> Pats bs' f a -> Bool
-eqPats NilP      NilP      = True
-eqPats (p :> ps) (q :> qs) = eqPat p q && eqPats ps qs
-eqPats _         _         = False
-
-instance Eq1 f         => Eq1 (Pats bs f)   where (==#) = eqPats
-instance (Eq1 f, Eq a) => Eq  (Pats bs f a) where (==)  = eqPats
-
-instance (Show1 f, Show a) => Show (Pats bs f a) where showsPrec = showsPrec1
-instance Show1 f => Show1 (Pats bs f) where
-  showsPrec1 _ NilP      = showString "NilP"
-  showsPrec1 d (p :> ps) = showParen (d > 5) $
-    showsPrec1 6 p . showString " :> " . showsPrec1 5 ps
-
-instance Functor f => Functor (Pats bs f) where
-  fmap _ NilP = NilP
-  fmap f (p :> ps) = fmap f p :> fmap f ps
-
-instance Foldable f => Foldable (Pats bs f) where
-  foldMap f (p :> ps) = foldMap f p `mappend` foldMap f ps
-  foldMap _ _    = mempty
-
-instance Traversable f => Traversable (Pats bs f) where
-  traverse f NilP = pure NilP
-  traverse f (p :> ps) = (:>) <$> traverse f p <*> traverse f ps
-
-instance Bound (Pats bs) where
-  NilP >>>= _ = NilP
-  (p :> ps) >>>= f = (p >>>= f) :> (ps >>>= f)
-
-
--- ** Path into Pats
-
-eqMPath :: MPath is -> MPath js -> Bool
-eqMPath (H m) (H n) = eqPath m n
-eqMPath (T p) (T q) = eqMPath p q
-eqMPath _     _     = False
-instance Eq (MPath is) where (==) = eqMPath
-
-compareMPath :: MPath is -> MPath js -> Ordering
-compareMPath (H m) (H n) = comparePath m n
-compareMPath (H _) (T _) = LT
-compareMPath (T p) (T q) = compareMPath p q
-compareMPath (T _) (H _) = GT
-instance Ord (MPath is) where compare = compareMPath
-
-instance Show (MPath is) where
-  showsPrec d (H m) = showParen (d > 10) $ showString "H " . showsPrec 11 m
-  showsPrec d (T p) = showParen (d > 10) $ showString "T " . showsPrec 11 p
-
--- instance Read (MPath is)
-
--- ** Path into Pat
-
-
-eqPath :: Path i -> Path j -> Bool
-eqPath V     V     = True
-eqPath L     L     = True
-eqPath (R m) (R n) = eqPath m n
-eqPath (C p) (C q) = eqMPath p q
-eqPath _     _     = False
-
-instance Eq (Path i) where (==) = eqPath
-
-comparePath :: Path i -> Path j -> Ordering
-comparePath V     V     = EQ
-comparePath V     _     = LT
-comparePath L     V     = GT
-comparePath L     L     = EQ
-comparePath L     _     = LT
-comparePath (R _) V     = GT
-comparePath (R _) L     = GT
-comparePath (R m) (R n) = comparePath m n
-comparePath (R _) (C _) = LT
-comparePath (C p) (C q) = compareMPath p q
-comparePath (C _) _     = GT
-
-instance Ord (Path i) where
-  compare V     V     = EQ
-  compare L     L     = EQ
-  compare L     _     = LT
-  compare (R _) L     = GT
-  compare (R m) (R n) = compare m n
-  compare (C p) (C q) = compare p q
-
-instance Show (Path i) where
-  showsPrec _ V     = showString "V"
-  showsPrec _ L     = showString "L"
-  showsPrec d (R m) = showParen (d > 10) $ showString "R " . showsPrec 11 m
-  showsPrec d (C p) = showParen (d > 10) $ showString "C " . showsPrec 11 p
-
-
diff --git a/examples/Overkill.hs b/examples/Overkill.hs
new file mode 100644
--- /dev/null
+++ b/examples/Overkill.hs
@@ -0,0 +1,287 @@
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE TypeOperators #-}
+module Exp where
+
+import Data.Vector as Vector hiding ((++), map)
+import Data.List as List
+import Data.Foldable
+import Data.Traversable
+import Data.Monoid (Monoid(..))
+import Control.Monad
+import Control.Monad.Trans.Class
+import Control.Applicative
+import Prelude hiding (foldr)
+import Prelude.Extras
+import GHC.Prim (Constraint(..))
+import Unsafe.Coerce
+import Bound
+
+infixl 9 :@
+infixr 5 :>
+
+-- little orphan instances
+instance Show1 Vector where showsPrec1 = showsPrec
+instance Eq1 Vector where (==#) = (==)
+
+data Exp a
+  = Var a
+  | Exp a :@ Exp a
+  | forall (b :: Index). Lam (Pat b Exp a) (Scope (Path b) Exp a)
+  | Let (Vector (Scope Int Exp a)) (Scope Int Exp a)
+
+data Index = VarI | WildI | AsI Index | ConI [Index]
+
+data Pat :: Index -> (* -> *) -> * -> * where
+  VarP  ::                             Pat VarI f a
+  WildP ::                             Pat WildI f a
+  AsP   :: Pat i f a                -> Pat (AsI i) f a
+  ConP  :: String    -> Pats bs f a -> Pat (ConI bs) f a
+  ViewP :: f a       -> Pat b f a   -> Pat b f a -- TODO: allow references to earlier variables
+
+data Pats :: [Index] -> (* -> *) -> * -> * where
+  NilP  :: Pats '[] f a
+  (:>) :: Pat b f a -> Pats bs f a -> Pats (b ': bs) f a
+
+data Path :: Index -> * where
+  V :: Path VarI
+  L :: Path (AsI a)
+  R :: Path a -> Path (AsI a)
+  C :: MPath as -> Path (ConI as)
+
+data MPath :: [Index] -> * where
+  H :: Path a   -> MPath (a ':as)
+  T :: MPath as -> MPath (a ':as)
+
+instance Functor Exp where
+  fmap = fmapDefault
+
+instance Foldable Exp where
+  foldMap = foldMapDefault
+
+instance Applicative Exp where
+  pure = Var
+  (<*>) = ap
+
+instance Traversable Exp where
+  traverse f (Var a)    = Var <$> f a
+  traverse f (x :@ y)   = (:@) <$> traverse f x <*> traverse f y
+  traverse f (Lam p e)  = Lam <$> traverse f p <*> traverse f e
+  traverse f (Let bs e) = Let <$> traverse (traverse f) bs <*> traverse f e
+
+instance Monad Exp where
+  return         = Var
+  Var a    >>= f = f a
+  (x :@ y) >>= f = (x >>= f) :@ (y >>= f)
+  Lam p e  >>= f = Lam (p >>>= f) (e >>>= f)
+  Let bs e >>= f = Let (fmap (>>>= f) bs) (e >>>= f)
+
+instance Eq a => Eq (Exp a) where (==) = (==#)
+instance Eq1 Exp where
+  Var a     ==# Var b     = a == b
+  (a :@ b)  ==# (c :@ d)  = a ==# c && b ==# d
+  Lam ps a  ==# Lam qs b  = eqPat ps qs && a ==# unsafeCoerce b -- eqPat proves equal shape
+  Let as a  ==# Let bs b  = as == bs && a ==# b
+  _         ==# _         = False
+
+instance Show a => Show (Exp a) where showsPrec = showsPrec1
+instance Show1 Exp where
+  showsPrec1 d (Var a)    = showParen (d > 10) $ showString "Var " . showsPrec 11 a
+  showsPrec1 d (a :@ b)   = showParen (d > 9) $ showsPrec1 9 a . showString " :@ " . showsPrec1 10 b
+  showsPrec1 d (Lam ps b) = showParen (d > 10) $ showString "Lam " . showsPrec1 11 ps . showChar ' ' . showsPrec1 11 b
+  showsPrec1 d (Let bs b) = showParen (d > 10) $ showString "Let " . showsPrec1 11 bs . showChar ' ' . showsPrec1 11 b
+
+-- * smart lam
+
+-- ** smart patterns
+
+data P a = forall b. P (Pat b Exp a) [a] (a -> Maybe (Path b))
+
+varp :: Eq a => a -> P a
+varp a = P VarP [a] (\v -> if a == v then Just V else Nothing)
+
+wildp :: P a
+wildp = P WildP [] (const Nothing)
+
+asp :: Eq a => a -> P a -> P a
+asp a (P p as f) = P (AsP p) (a:as) $ \v -> case f v of
+  Just b              -> Just (R b)
+  Nothing | a == v    -> Just L
+          | otherwise -> Nothing
+
+data Ps a = forall bs. Ps (Pats bs Exp a) [a] (a -> Maybe (MPath bs))
+
+conp :: String -> [P a] -> P a
+conp g ps = case go ps of
+  Ps qs as f -> P (ConP g qs) as (fmap C . f)
+  where
+    go :: [P a] -> Ps a
+    go [] = Ps NilP [] (const Nothing)
+    go (P p as f : xs) = case go xs of
+      Ps ps ass g -> Ps (p :> ps) (as ++ ass) $ \v ->
+        T <$> g v <|> H <$> f v
+
+-- * smart lam
+lam :: P a -> Exp a -> Exp a
+lam (P p _ f) t = Lam p (abstract f t)
+
+-- * smart let
+let_ :: Eq a => [(a, Exp a)] -> Exp a -> Exp a
+let_ bs b = Let (Vector.fromList $ map (abstr . snd) bs) (abstr b)
+  where vs  = map fst bs
+        abstr = abstract (`List.elemIndex` vs)
+
+-- * Pat
+
+-- ** A Kind of Shape
+
+eqPat :: (Eq1 f, Eq a) => Pat b f a -> Pat b' f a -> Bool
+eqPat VarP        VarP        = True
+eqPat WildP       WildP       = True
+eqPat (AsP p)     (AsP q)     = eqPat p q
+eqPat (ConP g ps) (ConP h qs) = g == h  && eqPats ps qs
+eqPat (ViewP e p) (ViewP f q) = e ==# f && eqPat p q
+
+instance Eq1 f   => Eq1 (Pat b f)        where (==#) = eqPat
+instance (Eq1 f, Eq a) => Eq (Pat b f a) where (==) = eqPat
+
+instance Show1 f => Show1 (Pat b f) where showsPrec1 = showsPrec
+instance (Show1 f, Show a) => Show (Pat b f a) where
+  showsPrec _ VarP        = showString "VarP"
+  showsPrec _ WildP       = showString "WildP"
+  showsPrec d (AsP p)     = showParen (d > 10) $ showString "AsP " . showsPrec 11 p
+  showsPrec d (ConP g ps) = showParen (d > 10) $ showString "ConP " . showsPrec 11 g . showChar ' ' . showsPrec 11 ps
+  showsPrec d (ViewP e p) = showParen (d > 10) $ showString "ViewP " . showsPrec1 11 e . showChar ' ' . showsPrec 11 p
+
+instance Functor f => Functor (Pat b f) where
+  fmap _ VarP = VarP
+  fmap _ WildP = WildP
+  fmap f (AsP p) = AsP (fmap f p)
+  fmap f (ConP g ps) = ConP g (fmap f ps)
+  fmap f (ViewP e p) = ViewP (fmap f e) (fmap f p)
+
+instance Foldable f => Foldable (Pat b f) where
+  foldMap f (AsP p)     = foldMap f p
+  foldMap f (ConP g ps) = foldMap f ps
+  foldMap f (ViewP e p) = foldMap f e `mappend` foldMap f p
+  foldMap _ _           = mempty
+
+instance Traversable f => Traversable (Pat b f) where
+  traverse _ VarP = pure VarP
+  traverse _ WildP = pure WildP
+  traverse f (AsP p) = AsP <$> traverse f p
+  traverse f (ConP g ps) = ConP g <$> traverse f ps
+  traverse f (ViewP e p) = ViewP <$> traverse f e <*> traverse f p
+
+instance Bound (Pat b) where
+  VarP      >>>= _ = VarP
+  WildP     >>>= _ = WildP
+  AsP p     >>>= f = AsP (p >>>= f)
+  ConP g ps >>>= f = ConP g (ps >>>= f)
+  ViewP e p >>>= f = ViewP (e >>= f) (p >>>= f)
+
+-- ** Pats
+
+
+eqPats :: (Eq1 f, Eq a) => Pats bs f a -> Pats bs' f a -> Bool
+eqPats NilP      NilP      = True
+eqPats (p :> ps) (q :> qs) = eqPat p q && eqPats ps qs
+eqPats _         _         = False
+
+instance Eq1 f         => Eq1 (Pats bs f)   where (==#) = eqPats
+instance (Eq1 f, Eq a) => Eq  (Pats bs f a) where (==)  = eqPats
+
+instance (Show1 f, Show a) => Show (Pats bs f a) where showsPrec = showsPrec1
+instance Show1 f => Show1 (Pats bs f) where
+  showsPrec1 _ NilP      = showString "NilP"
+  showsPrec1 d (p :> ps) = showParen (d > 5) $
+    showsPrec1 6 p . showString " :> " . showsPrec1 5 ps
+
+instance Functor f => Functor (Pats bs f) where
+  fmap _ NilP = NilP
+  fmap f (p :> ps) = fmap f p :> fmap f ps
+
+instance Foldable f => Foldable (Pats bs f) where
+  foldMap f (p :> ps) = foldMap f p `mappend` foldMap f ps
+  foldMap _ _    = mempty
+
+instance Traversable f => Traversable (Pats bs f) where
+  traverse f NilP = pure NilP
+  traverse f (p :> ps) = (:>) <$> traverse f p <*> traverse f ps
+
+instance Bound (Pats bs) where
+  NilP >>>= _ = NilP
+  (p :> ps) >>>= f = (p >>>= f) :> (ps >>>= f)
+
+
+-- ** Path into Pats
+
+eqMPath :: MPath is -> MPath js -> Bool
+eqMPath (H m) (H n) = eqPath m n
+eqMPath (T p) (T q) = eqMPath p q
+eqMPath _     _     = False
+instance Eq (MPath is) where (==) = eqMPath
+
+compareMPath :: MPath is -> MPath js -> Ordering
+compareMPath (H m) (H n) = comparePath m n
+compareMPath (H _) (T _) = LT
+compareMPath (T p) (T q) = compareMPath p q
+compareMPath (T _) (H _) = GT
+instance Ord (MPath is) where compare = compareMPath
+
+instance Show (MPath is) where
+  showsPrec d (H m) = showParen (d > 10) $ showString "H " . showsPrec 11 m
+  showsPrec d (T p) = showParen (d > 10) $ showString "T " . showsPrec 11 p
+
+-- instance Read (MPath is)
+
+-- ** Path into Pat
+
+
+eqPath :: Path i -> Path j -> Bool
+eqPath V     V     = True
+eqPath L     L     = True
+eqPath (R m) (R n) = eqPath m n
+eqPath (C p) (C q) = eqMPath p q
+eqPath _     _     = False
+
+instance Eq (Path i) where (==) = eqPath
+
+comparePath :: Path i -> Path j -> Ordering
+comparePath V     V     = EQ
+comparePath V     _     = LT
+comparePath L     V     = GT
+comparePath L     L     = EQ
+comparePath L     _     = LT
+comparePath (R _) V     = GT
+comparePath (R _) L     = GT
+comparePath (R m) (R n) = comparePath m n
+comparePath (R _) (C _) = LT
+comparePath (C p) (C q) = compareMPath p q
+comparePath (C _) _     = GT
+
+instance Ord (Path i) where
+  compare V     V     = EQ
+  compare L     L     = EQ
+  compare L     _     = LT
+  compare (R _) L     = GT
+  compare (R m) (R n) = compare m n
+  compare (C p) (C q) = compare p q
+
+instance Show (Path i) where
+  showsPrec _ V     = showString "V"
+  showsPrec _ L     = showString "L"
+  showsPrec d (R m) = showParen (d > 10) $ showString "R " . showsPrec 11 m
+  showsPrec d (C p) = showParen (d > 10) $ showString "C " . showsPrec 11 p
+
+-- ghci> let_ [("x",Var "y"),("y",Var "x" :@ Var "y")] $ lam (varp "z") (Var "z" :@ Var "y")
+-- ghci> lam (varp "x") (Var "x")
+-- ghci> lam (conp "Hello" [varp "x", wildp])) (Var "y")
diff --git a/examples/Simple.hs b/examples/Simple.hs
--- a/examples/Simple.hs
+++ b/examples/Simple.hs
@@ -1,5 +1,8 @@
 module Simple where
 
+-- this is a simple example where lambdas only bind a single variable at a time
+-- this directly corresponds to the usual de bruijn presentation
+
 import Data.Foldable
 import Data.Traversable
 import Control.Monad
@@ -8,24 +11,11 @@
 import Prelude.Extras
 import Bound
 
--- \ x -> x
--- ghci> lam "x" (Var "x")
--- Lam (Var (Bound ()))
-
--- \ x -> x y
--- ghci> lam "x" (Var "x" :@ Var "y")
--- Lam (Var (Bound ()) :@ Var (Free (Var "y")))
-
--- \ y -> \x -> x y
--- ghci> lam "y" (lam "x" (Var "x" :@ Var "y"))
--- Lam (Lam (Var (Bound ()) :@ Var (Free (Var (Bound ())))))
-
 infixl 9 :@
 
 data Exp a = Var a | Exp a :@ Exp a | Lam (Scope () Exp a)
   deriving (Eq,Ord,Show,Read)
 
-
 lam :: Eq a => a -> Exp a -> Exp a
 lam v b = Lam (abstract1 v b)
 
@@ -50,3 +40,16 @@
   Var a    >>= f = f a
   (x :@ y) >>= f = (x >>= f) :@ (y >>= f)
   Lam e    >>= f = Lam (e >>>= f)
+
+-- \ x -> x
+-- ghci> lam "x" (Var "x")
+-- Lam (Var (Bound ()))
+
+-- \ x -> x y
+-- ghci> lam "x" (Var "x" :@ Var "y")
+-- Lam (Var (Bound ()) :@ Var (Free (Var "y")))
+
+-- \ y -> \x -> x y
+-- ghci> lam "y" (lam "x" (Var "x" :@ Var "y"))
+-- Lam (Lam (Var (Bound ()) :@ Var (Free (Var (Bound ())))))
+