diff --git a/data-treify.cabal b/data-treify.cabal
--- a/data-treify.cabal
+++ b/data-treify.cabal
@@ -1,5 +1,5 @@
 Name:               data-treify
-Version:            0.3.2
+Version:            0.3.3
 Synopsis:           Reify a recursive data structure into an explicit graph.
 Description:	    This package is a (probably temporary) fork of Andy gill's data-reify package.
                     I've tweaked it for typed syntax representations for use with GADTs.
@@ -20,14 +20,14 @@
 		    Version 0.3 provided two versions of 'MuRef', the mono-typed version, for trees of a single type,
 		    and the dynamic-typed version, for trees of different types.
 		    .
-		    © 2009 Andy Gill; BSD3 license.
+		    © 2009-2012 Andy Gill & Conal Elliott; BSD3 license.
 
 Category:            Language, Data, Parsing, Reflection 
 License:             BSD3
 License-file:        LICENSE
-Author:              Andy Gill
-Maintainer:          Andy Gill <andygill@ku.edu>
-Copyright:           (c) 2009 Andy Gill
+Author:              Andy Gill & Conal Elliott
+Maintainer:          Conal Elliott <conal@conal.net>
+Copyright:           (c) 2009-2012 Andy Gill and Conal Elliott
 Homepage:            http://ittc.ku.edu/~andygill/data-reify.php
 Stability:	     alpha
 build-type: 	     Simple
@@ -43,50 +43,3 @@
        CustomTy
        Exp
   Ghc-Options:  -Wall
-
-
--- Library
---   Build-Depends: base, containers
---   Hs-Source-Dirs: src
---   Exposed-modules:
---        Data.Reify,
---        Data.Dynamic.Reify,
---        Data.Reify.Graph
---   Ghc-Options:  -Wall
-
-
--- Executable data-reify-test1
---   Build-Depends:  base
---   Main-Is:        Test1.hs
---   Hs-Source-Dirs: ., test
---   buildable: False
-
--- Executable data-reify-test2
---   Build-Depends:  base
---   Main-Is:        Test2.hs
---   Hs-Source-Dirs: ., test
---   buildable: False
-
--- Executable data-reify-test3
---   Build-Depends:  base
---   Main-Is:        Test3.hs
---   Hs-Source-Dirs: ., test
---   buildable: False
-
--- Executable data-reify-test4
---   Build-Depends:  base
---   Main-Is:        Test4.hs
---   Hs-Source-Dirs: ., test
---   buildable: False
-
--- Executable data-reify-test5
---   Build-Depends:  base
---   Main-Is:        Test5.hs
---   Hs-Source-Dirs: ., test
---   buildable: False
-
--- Executable data-reify-test6
---   Build-Depends:  base
---   Main-Is:        Test6.hs
---   Hs-Source-Dirs: ., test
---   buildable: False
diff --git a/src/Data/Reify/TGraph.hs b/src/Data/Reify/TGraph.hs
--- a/src/Data/Reify/TGraph.hs
+++ b/src/Data/Reify/TGraph.hs
@@ -1,13 +1,18 @@
 {-# LANGUAGE GADTs, ExistentialQuantification, FlexibleContexts
-           , UndecidableInstances
+           , UndecidableInstances, PatternGuards
   #-}
+{-# LANGUAGE ScopedTypeVariables #-} -- for bindEnv
+
 {-# OPTIONS_GHC -Wall #-}
 
 module Data.Reify.TGraph
-  ( ShowF(..), Id, V(..), Bind(..), Graph(..)
+  ( ShowF(..), Id, V(..), Bind(..), bindEnv, Graph(..)
   ) where
 
--- import Data.IsTy
+-- For bindEnv
+import Data.IsTy
+import Data.Proof.EQ
+import qualified Data.IntMap as I
 
 -- | Identifiers
 type Id = Int
@@ -17,10 +22,6 @@
 
 instance Eq (V ty a) where V i _ == V j _ = i == j
 
--- | Typed binding pair, parameterized by variable and node type
--- constructors. 
-data Bind ty n = forall a. Bind (V ty a) (n (V ty) a)
-
 class ShowF f where
   showF :: f a -> String                -- maybe Show a => 
 
@@ -35,6 +36,33 @@
 
 instance ShowF (n (V ty)) => Show (Bind ty n) where
   show (Bind v n) = showF v ++" = "++ showF n
+
+-- | Typed binding pair, parameterized by variable and node type
+-- constructors. 
+data Bind ty n = forall a. Bind (V ty a) (n (V ty) a)
+
+{-
+-- Slow version
+bindEnv' :: IsTy ty => [Bind ty n] -> (V ty a -> n (V ty) a)
+bindEnv' [] _ = error "bindEnv': ran out of bindings"
+bindEnv' (Bind (V i a) n : binds') v@(V i' a')
+  | Just Refl <- a `tyEq` a', i == i' = n
+  | otherwise                         = bindEnv' binds' v
+-}
+
+-- | Fast version, using an IntMap.
+-- Important: partially apply.
+bindEnv :: forall ty n a. IsTy ty => [Bind ty n] -> (V ty a -> n (V ty) a)
+bindEnv binds = \ (V i' a') -> extract a' (I.lookup i' m)
+ where
+   m :: I.IntMap (Bind ty n)
+   m = I.fromList [(i,b) | b@(Bind (V i _) _) <- binds]
+   extract :: ty a' -> Maybe (Bind ty n) -> n (V ty) a'
+   extract _ Nothing            = error "bindEnv: variable not found"
+   extract a' (Just (Bind (V _ a) n))
+     | Just Refl <- a `tyEq` a' = n
+     | otherwise                = error "bindEnv: wrong type"
+
 
 -- | Graph, described by bindings and a root variable
 data Graph ty n a = Graph [Bind ty n] (V ty a)
diff --git a/src/Exp.hs b/src/Exp.hs
--- a/src/Exp.hs
+++ b/src/Exp.hs
@@ -20,7 +20,7 @@
 import Data.Ty
 -- import CustomTy
 
-import Data.TReify
+import Data.TReify (MuRef(..),ShowF(..),V(..),Graph(..),Bind(..),Id,reifyGraph)
 
 {--------------------------------------------------------------------
     Expressions
@@ -56,16 +56,22 @@
   showF (ON o)    = unwords ["ON" ,showF o]
   showF (App a b) = unwords ["App",showF a,showF b]
 
-instance Show (E (V Ty) a) where
+-- instance Show (E (V Ty) a) where
+--   show (Op o) = show o
+--   show (u :^ v) = parens $ unwords [show u,show v]
+--   show (Let v a b) = unwords ["let",show v,"=",show a,"in",show b]
+--   show (Var v) = show v
+
+instance ShowF v => Show (E v a) where
   show (Op o) = show o
   show (u :^ v) = parens $ unwords [show u,show v]
-  show (Let v a b) = unwords ["let",show v,"=",show a,"in",show b]
-  show (Var v) = show v
-
+  show (Let v a b) = unwords ["let",showF v,"=",show a,"in",show b]
+  show (Var v) = showF v
 
 parens :: String -> String
 parens = ("(" ++) . (++ ")")
 
+-- TODO: showsPrec with infix and minimal parens
 
 instance MuRef Ty (E v) where
   type DeRef (E v) = N