diff --git a/Examples/ALaCarte.hs b/Examples/ALaCarte.hs
--- a/Examples/ALaCarte.hs
+++ b/Examples/ALaCarte.hs
@@ -4,7 +4,7 @@
 {-# LANGUAGE ViewPatterns #-}
 
 -- | Demonstration of the fact that "Language.Syntactic" has the same
--- functionality as /Data types á la carte/ (Wouter Swierstra, in
+-- functionality as /Data types à la carte/ (Wouter Swierstra, in
 -- /Journal of Functional Programming/, 2008)
 
 module ALaCarte where
diff --git a/Examples/MuFeldspar/Core.hs b/Examples/MuFeldspar/Core.hs
--- a/Examples/MuFeldspar/Core.hs
+++ b/Examples/MuFeldspar/Core.hs
@@ -156,16 +156,16 @@
 force :: Syntax a => a -> a
 force = resugar
 
-leT :: (Syntax a, Syntax b) => a -> (a -> b) -> b
-leT a f = sugar $ let_ (desugar a) (desugarN f)
+share :: (Syntax a, Syntax b) => a -> (a -> b) -> b
+share a f = sugar $ letBind (desugar a) (desugarN f)
 
 instance Eq (Data a)
   where
-    Data a == Data b = reifyHOAST a `eqLambda` reifyHOAST b
+    Data a == Data b = reify a `alphaEq` reify b
 
 instance Show (Data a)
   where
-    show (Data a) = render $ reifyHOAST a
+    show (Data a) = render $ reify a
 
 instance (Type a, Num a) => Num (Data a)
   where
diff --git a/Examples/MuFeldspar/Test.hs b/Examples/MuFeldspar/Test.hs
--- a/Examples/MuFeldspar/Test.hs
+++ b/Examples/MuFeldspar/Test.hs
@@ -13,7 +13,7 @@
 test1_3 = eval prog1 0 10
 
 prog2 :: Data Int -> Data Int
-prog2 a = leT (min a a) $ \b -> max b b
+prog2 a = share (min a a) $ \b -> max b b
 
 test2_1 = drawFeld prog2
 test2_2 = printFeld prog2
diff --git a/Language/Syntactic/Features/Binding.hs b/Language/Syntactic/Features/Binding.hs
--- a/Language/Syntactic/Features/Binding.hs
+++ b/Language/Syntactic/Features/Binding.hs
@@ -33,6 +33,11 @@
   where
     Variable :: Typeable a => VarId -> Variable (Full a)
 
+-- | Strict identifier comparison; i.e. no alpha equivalence
+instance ExprEq Variable
+  where
+    exprEq (Variable v1) (Variable v2) = v1==v2
+
 instance Render Variable
   where
     render (Variable v) = showVar v
@@ -48,6 +53,11 @@
   where
     Lambda :: (Typeable a, Typeable b) => VarId -> Lambda (b :-> Full (a -> b))
 
+-- | Strict identifier comparison; i.e. no alpha equivalence
+instance ExprEq Lambda
+  where
+    exprEq (Lambda v1) (Lambda v2) = v1==v2
+
 instance Render Lambda
   where
     renderPart [body] (Lambda v) = "(\\" ++ showVar v ++ " -> "  ++ body ++ ")"
@@ -60,45 +70,46 @@
 
 -- | Alpha-equivalence on 'Lambda' expressions. Free variables are taken to be
 -- equvalent if they have the same identifier.
-eqLambdaM :: ExprEq dom
+alphaEqM :: ExprEq dom
     => AST (Lambda :+: Variable :+: dom) a
     -> AST (Lambda :+: Variable :+: dom) b
     -> Reader [(VarId,VarId)] Bool
 
--- eqLambdaM (project -> Just (Variable v1)) (project -> Just (Variable v2)) = do  -- Not accepted by GHC-6.12
-eqLambdaM (Symbol (InjectR (InjectL (Variable v1)))) (Symbol (InjectR (InjectL (Variable v2)))) = do
+-- alphaEqM (project -> Just (Variable v1)) (project -> Just (Variable v2)) = do  -- Not accepted by GHC-6.12
+alphaEqM (Symbol (InjectR (InjectL (Variable v1)))) (Symbol (InjectR (InjectL (Variable v2)))) = do
     env <- ask
     case lookup v1 env of
       Nothing  -> return (v1==v2)   -- Free variables
       Just v2' -> return (v2==v2')
 
-eqLambdaM
+alphaEqM
 --     ((project -> Just (Lambda v1)) :$: a1)
 --     ((project -> Just (Lambda v2)) :$: a2)  -- Not accepted by GHC-6.12
     (Symbol (InjectL (Lambda v1)) :$: a1)
     (Symbol (InjectL (Lambda v2)) :$: a2)
-      = local ((v1,v2):) $ eqLambdaM a1 a2
+      = local ((v1,v2):) $ alphaEqM a1 a2
 
-eqLambdaM (f1 :$: a1) (f2 :$: a2) = do
-    e <- eqLambdaM f1 f2
-    if e then eqLambdaM a1 a2 else return False
+alphaEqM (f1 :$: a1) (f2 :$: a2) = do
+    e <- alphaEqM f1 f2
+    if e then alphaEqM a1 a2 else return False
 
-eqLambdaM
+alphaEqM
     (Symbol (InjectR (InjectR a)))
     (Symbol (InjectR (InjectR b)))
       = return (exprEq a b)
 
-eqLambdaM _ _ = return False
+alphaEqM _ _ = return False
 
 
 
-eqLambda :: ExprEq dom
+alphaEq :: ExprEq dom
     => AST (Lambda :+: Variable :+: dom) a
     -> AST (Lambda :+: Variable :+: dom) b
     -> Bool
-eqLambda a b = runReader (eqLambdaM a b) []
+alphaEq a b = runReader (alphaEqM a b) []
 
 
+
 -- | Evaluation of possibly open 'LambdaAST' expressions
 evalLambdaM :: (Eval dom, MonadReader [(VarId,Dynamic)] m) =>
     ASTF (Lambda :+: Variable :+: dom) a -> m a
@@ -179,7 +190,8 @@
 
 instance Render Let
   where
-    render Let = "Let"
+    renderPart []    Let = "Let"
+    renderPart [f,a] Let = "(" ++ unwords ["letBind",f,a] ++ ")"
 
 instance ToTree Let
   where
diff --git a/Language/Syntactic/Features/Binding/HigherOrder.hs b/Language/Syntactic/Features/Binding/HigherOrder.hs
--- a/Language/Syntactic/Features/Binding/HigherOrder.hs
+++ b/Language/Syntactic/Features/Binding/HigherOrder.hs
@@ -13,7 +13,7 @@
     , HOAST
     , lambda
     , lambdaN
-    , let_
+    , letBind
     , reifyM
     , reifyHOAST
     , Reifiable
@@ -52,11 +52,11 @@
 lambdaN = bindN lambda
 
 -- | Let binding
-let_ :: (Typeable a, Typeable b, Let :<: dom)
+letBind :: (Typeable a, Typeable b, Let :<: dom)
     => HOAST dom (Full a)
     -> (HOAST dom (Full a) -> HOAST dom (Full b))
     -> HOAST dom (Full b)
-let_ a f = inject Let :$: a :$: lambda f
+letBind a f = inject Let :$: a :$: lambda f
 
 
 
diff --git a/syntactic.cabal b/syntactic.cabal
--- a/syntactic.cabal
+++ b/syntactic.cabal
@@ -1,5 +1,5 @@
 Name:           syntactic
-Version:        0.3
+Version:        0.4
 Synopsis:       Generic abstract syntax, and utilities for embedded languages
 Description:    This library provides:
                 .