diff --git a/src/Language/Syntactic/Sharing/CodeMotion2.hs b/src/Language/Syntactic/Sharing/CodeMotion2.hs
--- a/src/Language/Syntactic/Sharing/CodeMotion2.hs
+++ b/src/Language/Syntactic/Sharing/CodeMotion2.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE DoRec #-}
 module Language.Syntactic.Sharing.CodeMotion2 
     ( codeMotion2
     , reifySmart2
@@ -6,6 +7,8 @@
 
 import Control.Monad.State
 import Control.Monad.Reader
+import Control.Monad.Writer
+import Control.Monad.RWS
 import qualified Data.Set as Set
 import qualified Data.Map as Map
 import Data.Array
@@ -36,8 +39,8 @@
 showNode :: NodeId -> String
 showNode n = "node:" ++ show n
 
-instance AlphaEq dom dom dom env => AlphaEq Node Node dom env 
-  where 
+instance AlphaEq dom dom dom env => AlphaEq Node Node dom env
+  where
     alphaEqSym (Node n1) _ (Node n2) _ = return (n1 == n2)
 
 instance Constrained Node
@@ -60,7 +63,6 @@
 
 type NodeDomain dom = (Node :+: dom) :|| Sat dom
 
-
 -- | A gathered sub-expression along with information used to decide where and
 -- if it should be shared.
 data Gathered dom = Gathered
@@ -68,13 +70,16 @@
         -- ^ The gathered expression.
     , geNodeId :: NodeId
         -- ^ The node id of the expression.
-    , geInfo :: [(NodeId, GatherInfo)] 
+    , geFreeVars :: Set.Set VarId
+        -- ^ Variables that occur free in the expression.
+    , geInfo :: [(NodeId, GatherInfo)]
         -- ^ A list of nodes which the gathered expression occurs in, which it
         -- should not be hoisted out of, along with the number of times it occurs
         -- in it and the union of all the scopes where the variable occurs.
     }
 
--- | An occurence count and a union of scopes for a gathered expression. Used 
+
+-- | An occurence count and a union of scopes for a gathered expression. Used
 -- for the heuristic for when to share an expression.
 data GatherInfo = GatherInfo
     { giCount :: Int
@@ -82,18 +87,32 @@
     }
   deriving Show
 
+
+newtype HashySet a = HashySet { unHashySet :: Map.Map Hash [a] }
+
+lookupWithHS :: ([a] -> b) -> Hash -> HashySet a -> b
+lookupWithHS f h (HashySet m) = case Map.lookup h m of
+    Nothing -> f []
+    Just as -> f as
+
+updateWithHS :: (Maybe [a] -> Maybe [a]) -> Hash -> HashySet a -> HashySet a
+updateWithHS f h (HashySet m) = HashySet $ Map.alter f h m
+
+emptyHS = HashySet Map.empty
+
+toListHS (HashySet m) = concatMap snd $ Map.toList m
+
 -- | A set of expressions used to keep track of gathered expression in `gather`
-newtype GatherSet dom = GatherSet {unGatherSet :: Map.Map Hash [Gathered dom]}
-        
+type GatherSet dom = HashySet (Gathered dom)
 
-lookupGS :: forall dom a 
+lookupGS :: forall dom a
     .  ( AlphaEq dom dom (NodeDomain dom) [(VarId,VarId)]
        , Equality dom)
     => GatherSet dom
     -> ASTF (NodeDomain dom) a
     -> Maybe (Gathered dom)
-lookupGS (GatherSet m) e = Map.lookup (exprHash e) m >>= look
-  where 
+lookupGS hs e = lookupWithHS look (exprHash e) hs
+  where
     look :: [Gathered dom] -> Maybe (Gathered dom)
     look [] = Nothing
     look (g:gs) | ASTB ge <- geExpr g
@@ -107,9 +126,9 @@
     => GatherSet dom
     -> Gathered dom
     -> GatherSet dom
-updateGS (GatherSet m) g
+updateGS hs g
     | ASTB ge <- geExpr g
-    = GatherSet $ Map.alter alt (exprHash ge) m
+    = updateWithHS alt (exprHash ge) hs
   where
     alt :: Maybe [Gathered dom] -> Maybe [Gathered dom]
     alt (Just gs) = Just $ ins gs
@@ -122,11 +141,13 @@
                 = g : xs
     ins (x:xs) = x : ins xs
 
-emptyGS = GatherSet $ Map.empty
+emptyGS :: GatherSet dom
+emptyGS = emptyHS
 
-toListGS (GatherSet m) = concatMap snd (Map.toList m)
+toListGS :: GatherSet dom -> [Gathered dom]
+toListGS gs = toListHS gs
 
-type RebuildEnv dom = 
+type RebuildEnv dom =
     ( Map.Map NodeId (ASTSAT dom)
         -- associates node ids with the AST they should be substituted by
     , Set.Set VarId
@@ -134,7 +155,7 @@
     , [NodeId]
         -- nodes that have been encountered
     )
-  
+
 type RebuildMonad dom a = ReaderT (RebuildEnv dom) (State VarId) a
 
 
@@ -169,6 +190,7 @@
 
 codeMotion2 :: forall dom a
     .  ( ConstrainedBy dom Typeable
+       , AlphaEq dom dom dom [(VarId,VarId)]
        , AlphaEq dom dom (NodeDomain dom) [(VarId,VarId)]
        , Equality dom
        )
@@ -177,10 +199,10 @@
     -> MkInjDict dom
     -> ASTF dom a
     -> State VarId (ASTF dom a)
-codeMotion2 hoistOver pd mkId a = do
-    let (gm, a') = gather hoistOver pd a
-    rebuild pd mkId (toListGS gm) a'
-
+codeMotion2 hoistOver pd mkId a = rebuild pd mkId garr a'
+  where
+    (garr, a') = gather hoistOver pd a
+ 
 type ShareInfo dom = (NodeId, ASTSAT (NodeDomain dom), GatherInfo)
 
 data ShareMaybe dom a
@@ -195,22 +217,17 @@
        )
     => PrjDict dom
     -> MkInjDict dom
-    -> [Gathered dom]
+    -> Array NodeId (Gathered dom)
     -> ASTF (NodeDomain dom) a
     -> State VarId (ASTF dom a)
-rebuild pd mkId gs (Sym (C' (InjL _))) = error ""
-rebuild pd mkId gs a = runRebuild $ rebuild' 0 a
+rebuild pd mkId nodes (Sym (C' (InjL _))) = error ""
+rebuild pd mkId nodes a = runRebuild $ rebuild' 0 a
   where
-    nodes :: Array NodeId (Gathered dom)
-    nodes = array
-        (1, maximum (0:(Prelude.map geNodeId gs)))
-        (zip (Prelude.map geNodeId gs) gs)
-
     nodeExpr :: NodeId -> ASTSAT (NodeDomain dom)
     nodeExpr n = geExpr (nodes ! n)
 
-    freeVars :: Array NodeId (Set.Set VarId)
-    freeVars = nodesFreeVars pd nodes
+    freeVars :: NodeId -> Set.Set VarId
+    freeVars n = geFreeVars (nodes ! n)
 
     nodeDeps :: Array NodeId (Set.Set NodeId)
     nodeDeps = nodeDepsArray
@@ -220,13 +237,13 @@
         nodeDepsNode :: NodeId -> Set.Set NodeId
         nodeDepsNode 0 = nodeDepsExp a
         nodeDepsNode n = liftASTB nodeDepsExp $ geExpr (nodes ! n)
-        
+
         nodeDepsExp :: AST (NodeDomain dom) b -> Set.Set NodeId
         nodeDepsExp (Sym (C' (InjR _))) = Set.empty
         nodeDepsExp (Sym (C' (InjL (Node n)))) = Set.insert n (nodeDepsArray ! n)
         nodeDepsExp (s :$ b) = Set.union (nodeDepsExp s) (nodeDepsExp b)
 
-    -- | Computes a list of nodes that should be considered for sharing at a 
+    -- | Computes a list of nodes that should be considered for sharing at a
     -- particular node. Must return a ShareInfo corresponding to any node
     -- that might be encounter in direct sub-expression of the node that has
     -- not already been considered at a parent node. Otherwise we will not know
@@ -242,11 +259,11 @@
             | (il,gi) <- geInfo g
             --, i <- elemIndex il seenNodes
                 -- must be shared inside `il`
-            , Set.null (freeVars ! n `Set.difference` bv)
+            , Set.null (freeVars n `Set.difference` bv)
                 -- any free variables in the sub-expression must be bound
             , f n
             ]
-    
+
     rebuild' :: forall b
         .  NodeId
         -> ASTF (NodeDomain dom) b
@@ -264,7 +281,7 @@
                     return (Sym lam :$ a')
     rebuild' n (Sym (C' (InjR s))) = return $ Sym s
     rebuild' n a = addSeenNode n $ shareExprsIn n a
-    
+
     shareExprsIn :: forall b
         .  NodeId
         -> ASTF (NodeDomain dom) b
@@ -276,7 +293,7 @@
         let considered = nodesToConsider (\n' -> n' /= n && not (Map.member n' nodeMap) && Set.member n' (nodeDeps ! n)) bv seenNodes
         let sorted = sortBy (compare `on` (\(n,_,_) -> n)) considered
         shareEm sorted a
-    
+
     shareEm
         :: [ShareInfo dom]
         -> ASTF (NodeDomain dom) b
@@ -306,7 +323,7 @@
         b' <- fixNodeExpr b
         s' <- fixNodeExprSub s
         return (s' :$ b')
-        
+ 
     fixNodeExpr :: forall b . ASTF (NodeDomain dom) b -> RebuildMonad dom (ASTF dom b)
     fixNodeExpr (ns@(Sym (C' (InjL (Node n))))) = do
         nodeMap <- getNodeExprMap
@@ -325,26 +342,6 @@
     heuristic :: Set.Set VarId -> GatherInfo -> ASTF (NodeDomain dom) b -> Bool
     heuristic bv gi b = not (isVariable pd b) && (giCount gi > 1 || not (Set.null (giScopes gi `Set.difference` bv)))
 
--- | Given a array of nodes calculates the set of free variables in the
--- sub-expression each 
-nodesFreeVars :: forall dom
-    .  PrjDict dom 
-    -> Array NodeId (Gathered dom) 
-    -> Array NodeId (Set.Set VarId)
-nodesFreeVars pd nodes = freeVars
-  where
-    freeVars = array (bounds nodes) [(n, freeVarsNode n) | n <- indices nodes]
-
-    freeVarsNode :: NodeId -> Set.Set VarId
-    freeVarsNode n = liftASTB freeVarsExp $ geExpr (nodes ! n)
-    
-    freeVarsExp :: AST (NodeDomain dom) a -> Set.Set VarId
-    freeVarsExp (Sym (C' (InjR var))) | Just v <- prjVariable pd var = Set.singleton v
-    freeVarsExp (Sym (C' (InjR lam)) :$ b) | Just v <- prjLambda pd lam = Set.delete v (freeVarsExp b)
-    freeVarsExp (Sym (C' (InjR _))) = Set.empty
-    freeVarsExp (Sym (C' (InjL (Node n)))) = freeVars ! n
-    freeVarsExp (s :$ b) = Set.union (freeVarsExp s) (freeVarsExp b)
-
 inlineAll :: forall dom a
     .  ConstrainedBy dom Typeable
     => (NodeId -> ASTSAT (NodeDomain dom))
@@ -364,105 +361,247 @@
               Just a  -> go a
 
 
-type GatherEnv = 
-    ( [NodeId]    
+type GatherEnv =
+    ( [NodeId]
         -- List of nodes upwards in the syntax tree that cannot be hoisted over
     , Set.Set VarId
         -- Varibles in scope
     )
-type GatherState dom = 
-    ( GatherSet dom -- Set of expressions that have been recorded
-    , NodeId -- Node counter.
-    )
 
-type GatherMonad dom a = ReaderT GatherEnv (State (GatherState dom)) a
+type Additional = Map.Map NodeId [(NodeId, GatherInfo)]
 
-runGather :: GatherSet dom -> GatherMonad dom a -> (GatherSet dom, a)
-runGather s gather = (gm,a)
-  where 
-    (a,(gm,n')) = runState (runReaderT gather ([0], Set.empty)) (s,1)
+data GatherState dom = GatherState
+    { gatherSet :: GatherSet dom -- Set of expressions that have been recorded
+    , nodeCounter :: NodeId
+    , lambdaTable :: LambdaTable dom
+    , additionals :: Map.Map NodeId [(NodeId, GatherInfo)]
+    }
 
+data LambdaInfo dom = LambdaInfo
+    { liExpr :: ASTSAT dom
+    , liLambdaNodeId :: NodeId
+    }
+
+type GatherMonad dom a = RWS GatherEnv (Set.Set VarId) (GatherState dom) a
+
+runGather :: GatherMonad dom a -> (GatherState dom, a)
+runGather gather = (s', a)
+  where
+    (a,s',w) = runRWS gather ([0], Set.empty) (GatherState emptyGS 1 emptyHS Map.empty)
+
+type LambdaTable dom = HashySet (LambdaInfo dom)
+
+lookupLT :: forall dom a
+    . ( AlphaEq dom dom dom [(VarId,VarId)]
+      , Equality dom)
+    => Hash
+    -> ASTF dom a
+    -> LambdaTable dom
+    -> Maybe (LambdaInfo dom)
+lookupLT h e t = lookupWithHS look h t
+  where
+    look :: [LambdaInfo dom] -> Maybe (LambdaInfo dom)
+    look [] = Nothing
+    look (li:xs) | liftASTB alphaEq (liExpr li) e
+                 = Just li
+    look (x:xs) = look xs
+
+-- | Note: Assumes the given lambda is not already in the map
+insertLT :: forall dom a
+    . ( Sat dom a
+      , AlphaEq dom dom dom [(VarId,VarId)]
+      , Equality dom)
+    => Hash
+    -> ASTF dom a
+    -> NodeId
+    -> LambdaTable dom
+    -> LambdaTable dom
+insertLT h e n t = updateWithHS ins h t
+  where
+    ins :: Maybe [LambdaInfo dom] -> Maybe [LambdaInfo dom]
+    ins (Just xs) = Just (LambdaInfo (ASTB e) n : xs)
+    ins Nothing = Just [LambdaInfo (ASTB e) n]
+
+
 getInnerLimit :: GatherMonad dom NodeId
 getInnerLimit = liftM (head . fst) ask
 
 getScope :: GatherMonad dom (Set.Set VarId)
 getScope = liftM snd ask
 
+getLambdaTable :: GatherMonad dom (LambdaTable dom)
+getLambdaTable = liftM lambdaTable get
+
+putLambdaTable :: LambdaTable dom -> GatherMonad dom ()
+putLambdaTable lt = do
+    st <- get
+    put (st { lambdaTable = lt })
+
 addInnerLimit :: NodeId -> GatherMonad dom a -> GatherMonad dom a
 addInnerLimit n = local (\(ns,vs) -> (n:ns,vs))
 
 addScopeVar :: VarId -> GatherMonad dom a -> GatherMonad dom a
-addScopeVar v = local (\(ns,vs) -> (ns, Set.insert v vs ))
+addScopeVar v = censor (Set.delete v) . local (\(ns,vs) -> (ns, Set.insert v vs ))
 
 -- | Convert an expression to a graph representation where each set of
 -- alpha-equivalent sub-expressions share a node. Occurence counts for the
 -- sub-expressions, and other information is also recorded.
-gather :: forall dom a 
+gather :: forall dom a
     .  ( ConstrainedBy dom Typeable
        , AlphaEq dom dom (NodeDomain dom) [(VarId,VarId)]
+       , AlphaEq dom dom dom [(VarId,VarId)]
        , Equality dom
        )
     => (forall c. ASTF dom c -> Bool)
     -> PrjDict dom
     -> ASTF dom a
-    -> (GatherSet dom, ASTF (NodeDomain dom) a)
-gather hoistOver pd a@(Sym s) | Dict <- exprDict a = (emptyGS, Sym (C' (InjR s)))
-gather hoistOver pd a | Dict <- exprDict a
-                      = runGather emptyGS (gatherRec (hoistOver a) a)
+    -> (Array NodeId (Gathered dom), ASTF (NodeDomain dom) a)
+gather hoistOver pd a@(Sym s) | Dict <- exprDict a = (array (1,0) [], Sym (C' (InjR s)))
+gather hoistOver pd a = (gatheredArr, a')
   where
+    (st,a') | Dict <- exprDict a = runGather (gatherRec (hoistOver a) a)
+
+    gths = toListGS (gatherSet st)
+
+    idx = map geNodeId gths
+
+    adArr :: Array NodeId [(NodeId, GatherInfo)]
+    adArr = accumArray (++) []
+        (1, nodeCounter st - 1)
+        ((Map.assocs (additionals st)) ++ [(n, []) | n <- [1..(nodeCounter st - 1)]])
+
+    preGatheredArr :: Array NodeId (Gathered dom)
+    preGatheredArr = array
+        (1, nodeCounter st - 1)
+        (zip idx gths)
+
+    gatheredArr :: Array NodeId (Gathered dom)
+    gatheredArr = array
+        (1, nodeCounter st - 1)
+        (zip idx (Prelude.map withAdditionals gths))
+
+    withAdditionals g = g { geInfo = info}
+      where
+        info = mergeInfos
+                (geInfo g)
+                (Map.findWithDefault [] (geNodeId g) propagateAdditionals)
+
+    propagateAdditionals :: Additional
+    propagateAdditionals = propAddsExpr 0 a' $ additionals st
+      where
+        propAddsNode :: NodeId -> Additional -> Additional
+        propAddsNode n ad = liftASTB (propAddsExpr n) (geExpr (preGatheredArr ! n)) ad
+
+        propAddsExpr :: NodeId -> AST (NodeDomain dom) b -> Additional -> Additional
+        propAddsExpr n (Sym s) ad = ad
+        propAddsExpr n (s :$ Sym (C' (InjL (Node n')))) ad = propAddsNode n' ad'
+          where
+            ad' = Map.insertWith mergeInfos n' (Map.findWithDefault [] n ad) ad
+
+    applyAdditionals :: [(NodeId, GatherInfo)] -> Gathered dom -> Gathered dom
+    applyAdditionals ad g = g { geInfo = mergeInfos ad (geInfo g) }
+
+    varHash :: Map.Map VarId Hash
+    varHash = lambdaHashes pd a
+
     gather' :: Bool -> ASTF dom b -> GatherMonad dom (ASTF (NodeDomain dom) b)
+    gather' h a@(Sym lam :$ _) | Just v <- prjLambda pd lam
+                               , Dict <- exprDict a = do
+        lt <- getLambdaTable
+        let hash = fromJust (Map.lookup v varHash)
+        case lookupLT hash a lt of
+            Just li -> do
+                anotherCopyOf (liLambdaNodeId li)
+                return $ Sym $ C' $ InjL $ Node $ liLambdaNodeId li
+            Nothing -> do
+                rec
+                    (a',fv) <- listen $ addInnerLimitIf (not h) n $ addScopeVar v $ gatherRec (hoistOver a) a
+                    n <- recordExpr fv a'
+                putLambdaTable (insertLT hash a n lt)
+                return $ Sym $ C' $ InjL $ Node n
     gather' h a | Dict <- exprDict a = do
-        (a',n) <-
-          mfix (\(~(a',n)) -> do
-            a' <- addInnerLimitIf (not h) n $ gatherRec (hoistOver a) a 
-            n <- recordExpr a'
-            return (a',n)
-          )
+        rec
+            (a',fv) <- listen $ addInnerLimitIf (not h) n $ gatherRec (hoistOver a) a
+            n <- recordExpr fv a'
         return $ Sym $ C' $ InjL $ Node n
 
     addInnerLimitIf True n m = addInnerLimit n m
     addInnerLimitIf _    n m = m
 
-    gatherRec 
+    gatherRec
         :: (Sat dom (DenResult b))
         => Bool
         -> AST dom b
-        -> GatherMonad dom (AST (NodeDomain dom) b) 
-    gatherRec h (Sym lam :$ b) | Just v <- prjLambda pd lam = do
-        b' <- addScopeVar v $ gather' h b
-        return ((Sym (C' (InjR lam))) :$ b')
+        -> GatherMonad dom (AST (NodeDomain dom) b)
+    gatherRec h (Sym var) | Just v <- prjVariable pd var = do
+            tell (Set.singleton v)
+            return $ Sym $ C' $ InjR var
     gatherRec h (Sym s) = return $ Sym $ C' $ InjR s
-    gatherRec h (s :$ b) = do
+    gatherRec h (s :$ b) | Dict <- exprDict b = do
         b' <- gather' h b
         s' <- gatherRec h s
         return (s' :$ b')
 
-    recordExpr :: ASTF (NodeDomain dom) b -> GatherMonad dom NodeId
-    recordExpr a | Dict <- exprDict a = do
-        (s,n) <- get
+    anotherCopyOf :: NodeId -> GatherMonad dom ()
+    anotherCopyOf n = do
+        st <- get
+        let s = gatherSet st
+        let ad = additionals st
         innerLimit <- getInnerLimit
         scope <- getScope
+        put (st { additionals = Map.insertWith mergeInfos n [(innerLimit, GatherInfo 1 scope)] ad })
+
+    recordExpr :: Set.Set VarId -> ASTF (NodeDomain dom) b -> GatherMonad dom NodeId
+    recordExpr fv a | Dict <- exprDict a = do
+        st <- get
+        let s = gatherSet st
+        let n = nodeCounter st
+        innerLimit <- getInnerLimit
+        scope <- getScope
         case lookupGS s a of
             Just ge -> do
-                let ge' = ge { geInfo = updateInfo scope (geInfo ge) innerLimit }
-                put (updateGS s ge', n)
+                let ge' = ge { geInfo = updateInfo innerLimit (GatherInfo 1 scope) (geInfo ge) }
+                put (st { gatherSet = updateGS s ge' })
                 return (geNodeId ge)
             Nothing -> do
-                let ge = Gathered { geExpr = ASTB a , geNodeId = n , geInfo = [(innerLimit, GatherInfo { giCount = 1 , giScopes = scope })] }
-                put (updateGS s ge, n+1)
+                let ge = Gathered { geExpr = ASTB a , geNodeId = n , geFreeVars = fv , geInfo = [(innerLimit, GatherInfo { giCount = 1 , giScopes = scope })] }
+                put (st { gatherSet = updateGS s ge, nodeCounter = n+1 })
                 return n
 
-updateInfo :: Set.Set VarId -> [(NodeId, GatherInfo)] -> NodeId -> [(NodeId, GatherInfo)]
-updateInfo scope [] n = [(n, GatherInfo { giCount = 1 , giScopes = scope })]
-updateInfo scope ((n,gi):xs) n' | n == n' = (n, gi') : xs
+mergeInfos :: [(NodeId, GatherInfo)] -> [(NodeId, GatherInfo)] -> [(NodeId, GatherInfo)]
+mergeInfos [] ys = ys
+mergeInfos (x:xs) ys = mergeInfos xs (uncurry updateInfo x ys)
+
+updateInfo :: NodeId -> GatherInfo -> [(NodeId, GatherInfo)] -> [(NodeId, GatherInfo)]
+updateInfo il gi [] = [(il, gi)]
+updateInfo il (GatherInfo c scope) ((n,gi):xs) | n == il = (n, gi') : xs
   where
-    gi' = gi { giCount = giCount gi + 1 , giScopes = Set.union (giScopes gi) scope }
-updateInfo scope (x:xs) n' = x : updateInfo scope xs n'
+    gi' = gi { giCount = giCount gi + c , giScopes = Set.union (giScopes gi) scope }
+updateInfo il gi (x:xs) = x : updateInfo il gi xs
 
 
+lambdaHashes :: forall dom a
+    .  (Equality dom)
+    => PrjDict dom
+    -> ASTF dom a
+    -> Map.Map VarId Hash
+lambdaHashes pd a = execWriter (lambdaHashes' a)
+  where
+    lambdaHashes' :: AST dom b -> Writer (Map.Map VarId Hash) Hash
+    lambdaHashes' (Sym lam :$ b) | Just v <- prjLambda pd lam = do
+        h' <- lambdaHashes' b
+        tell (Map.singleton v h')
+        return $ hashInt 1 `combine` exprHash (Sym lam) `combine` h'
+    lambdaHashes' (s :$ b) = do
+        hs <- lambdaHashes' s
+        hb <- lambdaHashes' b
+        return $ hashInt 1 `combine` hs `combine` hb
+    lambdaHashes' s = return $ hashInt 0 `combine` exprHash s
+
 -- | Like 'reify' but with common sub-expression elimination and variable hoisting
 reifySmart2 :: forall dom p pVar a
     .  ( AlphaEq dom dom (NodeDomain (FODomain dom p pVar)) [(VarId,VarId)]
+       , AlphaEq dom dom (FODomain dom p pVar) [(VarId,VarId)]
        , Equality dom
        , Syntactic a
        , Domain a ~ HODomain dom p pVar
diff --git a/syntactic.cabal b/syntactic.cabal
--- a/syntactic.cabal
+++ b/syntactic.cabal
@@ -1,5 +1,5 @@
 Name:           syntactic
-Version:        1.12.1
+Version:        1.13
 Synopsis:       Generic abstract syntax, and utilities for embedded languages
 Description:    This library provides:
                 .