diff --git a/src/Language/Syntactic/Constructs/Binding.hs b/src/Language/Syntactic/Constructs/Binding.hs
--- a/src/Language/Syntactic/Constructs/Binding.hs
+++ b/src/Language/Syntactic/Constructs/Binding.hs
@@ -10,6 +10,8 @@
 import qualified Control.Monad.Identity as Monad
 import Control.Monad.Reader
 import Data.Ix
+import Data.Set (Set)
+import qualified Data.Set as Set
 import Data.Tree
 import Data.Typeable
 
diff --git a/src/Language/Syntactic/Sharing/SimpleCodeMotion.hs b/src/Language/Syntactic/Sharing/SimpleCodeMotion.hs
--- a/src/Language/Syntactic/Sharing/SimpleCodeMotion.hs
+++ b/src/Language/Syntactic/Sharing/SimpleCodeMotion.hs
@@ -66,6 +66,8 @@
     subst :: AST dom c -> AST dom c
     subst (f :$ a) = subst f :$ substitute x y a
     subst a = a
+  -- Note: Since `codeMotion` only uses `substitute` to replace sub-expressions
+  -- with fresh variables, there's no risk of capturing.
 
 -- | Count the number of occurrences of a sub-expression
 count :: forall dom a b
@@ -92,22 +94,27 @@
         -- expression
     }
 
-independent :: PrjDict dom -> Env dom -> AST dom a -> Bool
-independent pd env (Sym (prjVariable pd -> Just v)) = not (v `member` dependencies env)
-independent pd env (f :$ a) = independent pd env f && independent pd env a
-independent _ _ _ = True
-
 isVariable :: PrjDict dom -> ASTF dom a -> Bool
 isVariable pd (Sym (prjVariable pd -> Just _)) = True
 isVariable pd _ = False
 
+-- | Get the set of free variables in an expression
+freeVars :: PrjDict dom -> AST dom sig -> Set VarId
+freeVars pd (Sym var)
+    | Just v <- prjVariable pd var = Set.singleton v
+freeVars pd (Sym lam :$ body)
+    | Just v <- prjLambda pd lam = Set.delete v (freeVars pd body)
+freeVars pd (s :$ a) = Set.union (freeVars pd s) (freeVars pd a)
+freeVars _ _ = Set.empty
+
 -- | Checks whether a sub-expression in a given environment can be lifted out
 liftable :: PrjDict dom -> Env dom -> ASTF dom a -> Bool
-liftable pd env a = independent pd env a && not (isVariable pd a) && heuristic
+liftable pd env a = independent && not (isVariable pd a) && heuristic
     -- Lifting dependent expressions is semantically incorrect
     -- Lifting variables would cause `codeMotion` to loop
   where
-    heuristic = inLambda env || (counter env (ASTE a) > 1)
+   independent = Set.null $ Set.intersection (freeVars pd a) (dependencies env)
+   heuristic   = inLambda env || (counter env (ASTE a) > 1)
 
 
 
diff --git a/syntactic.cabal b/syntactic.cabal
--- a/syntactic.cabal
+++ b/syntactic.cabal
@@ -1,5 +1,5 @@
 Name:           syntactic
-Version:        1.16.1
+Version:        1.16.2
 Synopsis:       Generic abstract syntax, and utilities for embedded languages
 Description:    This library provides:
                 .