diff --git a/src/Eval.hs b/src/Eval.hs
index a69f210..2b93c1d 100644
--- a/src/Eval.hs
+++ b/src/Eval.hs
@@ -3,8 +3,11 @@ module Eval where
 import Parser
 import Research
 
-import Data.List (partition, (\\))
-import Data.Map  (Map)
+import           Data.List   (partition, (\\))
+import           Data.Map    (Map)
+import           Data.Set    (Set)
+
+import qualified Data.Foldable as F
 import qualified Data.Map as Map
 import qualified Data.Set as Set
 
@@ -63,17 +66,17 @@ elimLambda :: TricuAST -> TricuAST
 elimLambda = go
   where
     go term
-      | etaReduction term   = elimLambda $ etaReduceResult term
+      | etaReduction term   = go (etaReduceResult term)
       | triagePattern term  = _TRI
       | composePattern term = _B
-      | lambdaList term     = elimLambda $ lambdaListResult term
+      | lambdaList term     = go (lambdaListResult term)
       | nestedLambda term   = nestedLambdaResult term
       | application term    = applicationResult term
       | otherwise           = term
 
+    -- patterns
     etaReduction (SLambda [v] (SApp f (SVar x))) = v == x && not (isFree v f)
     etaReduction _ = False
-    etaReduceResult (SLambda [_] (SApp f _)) = f
 
     triagePattern (SLambda [a] (SLambda [b] (SLambda [c] body))) = body == triageBody a b c
     triagePattern _ = False
@@ -83,58 +86,68 @@ elimLambda = go
 
     lambdaList (SLambda [_] (SList _)) = True
     lambdaList _ = False
-    lambdaListResult (SLambda [v] (SList xs)) = SLambda [v] (foldr wrapTLeaf TLeaf xs)
-    wrapTLeaf m r = SApp (SApp TLeaf m) r
 
     nestedLambda (SLambda (_:_) _) = True
     nestedLambda _ = False
-    nestedLambdaResult (SLambda (v:vs) body)
-      | null vs   = toSKI v (elimLambda body)
-      | otherwise = elimLambda (SLambda [v] (SLambda vs body))
 
     application (SApp _ _) = True
     application _ = False
-    applicationResult (SApp f g) = SApp (elimLambda f) (elimLambda g)
 
+    -- rewrites
+    etaReduceResult (SLambda [_] (SApp f _)) = f
+
+    lambdaListResult (SLambda [v] (SList xs)) =
+      SLambda [v] (foldr wrapTLeaf TLeaf xs)
+      where
+        wrapTLeaf m r = SApp (SApp TLeaf m) r
+
+    nestedLambdaResult (SLambda (v:vs) body)
+      | null vs   = toSKI v (go body)
+      | otherwise = go (SLambda [v] (SLambda vs body))
+
+    applicationResult (SApp f g) = SApp (go f) (go g)
+
+    -- SKI translation
+    toSKI x t
+      | not (isFree x t) = SApp _K t
     toSKI x (SVar y)
       | x == y           = _I
       | otherwise        = SApp _K (SVar y)
-    toSKI x t@(SApp n u)
-      | not (isFree x t) = SApp _K t
-      | otherwise        = SApp (SApp _S (toSKI x n)) (toSKI x u)
-    toSKI x (SList xs)
-      | not (isFree x (SList xs)) = SApp _K (SList xs)
-      | otherwise = SList (map (toSKI x) xs)
-    toSKI x t
-      | not (isFree x t) = SApp _K t
-      | otherwise        = errorWithoutStackTrace "Unhandled toSKI conversion"
+    toSKI x (SApp n u)   = SApp (SApp _S (toSKI x n)) (toSKI x u)
+    toSKI x (SList xs) =
+      let free = any (isFree x) xs
+      in if not free then SApp _K (SList xs) else SList (map (toSKI x) xs)
+    toSKI _ t            = errorWithoutStackTrace $ "Unhandled toSKI conversion: " ++ show t
 
-    -- Combinators and special forms
+    -- combinators and special forms
     _S   = parseSingle "t (t (t t t)) t"
     _K   = parseSingle "t t"
     _I   = parseSingle "t (t (t t)) t"
     _B   = parseSingle "t (t (t t (t (t (t t t)) t))) (t t)"
     _TRI = parseSingle "t (t (t t (t (t (t t t))))) t"
-    
-    -- Pattern bodies
-    triageBody a b c = SApp (SApp TLeaf (SApp (SApp TLeaf (SVar a)) (SVar b))) (SVar c)
-    composeBody f g x = SApp (SVar f) (SApp (SVar g) (SVar x))
+
+    -- pattern bodies
+    triageBody a b c   = SApp (SApp TLeaf (SApp (SApp TLeaf (SVar a)) (SVar b))) (SVar c)
+    composeBody f g x  = SApp (SVar f) (SApp (SVar g) (SVar x))
 
 isFree :: String -> TricuAST -> Bool
 isFree x = Set.member x . freeVars
 
-freeVars :: TricuAST -> Set.Set String
-freeVars (SVar    v    ) = Set.singleton v
-freeVars (SList   s    ) = foldMap freeVars s
-freeVars (SLambda v b  ) = foldr Set.delete (freeVars b) v
-freeVars (SApp    f a  ) = freeVars f <> freeVars a
-freeVars (TFork   l r  ) = freeVars l <> freeVars r
-freeVars (SDef   _ _ b)  = freeVars b
-freeVars (TStem   t    ) = freeVars t
-freeVars (SInt    _    ) = Set.empty
-freeVars (SStr    _    ) = Set.empty
-freeVars  TLeaf          = Set.empty
-freeVars  _              = Set.empty
+freeVars :: TricuAST -> Set String
+freeVars (SVar v)        = Set.singleton v
+freeVars (SInt _)        = Set.empty
+freeVars (SStr _)        = Set.empty
+freeVars TLeaf           = Set.empty
+freeVars SEmpty          = Set.empty
+freeVars (SImport _ _)   = Set.empty
+freeVars (SList xs)      = F.foldMap freeVars xs
+freeVars (SApp f a)      = freeVars f <> freeVars a
+freeVars (TFork l r)     = freeVars l <> freeVars r
+freeVars (TStem t)       = freeVars t
+-- lambda binds all names in its vector
+freeVars (SLambda vs b)  = freeVars b `Set.difference` Set.fromList vs
+-- -- definition binds the function name and its parameters in the body
+freeVars (SDef f vs b)   = freeVars b `Set.difference` Set.fromList (f:vs)
 
 reorderDefs :: Env -> [TricuAST] -> [TricuAST]
 reorderDefs env defs