diff --git a/1_k/1_lambda/lesson_2.5/lambda.k b/1_k/1_lambda/lesson_2.5/lambda.k
index 26242e66..932d42e0 100644
--- a/1_k/1_lambda/lesson_2.5/lambda.k
+++ b/1_k/1_lambda/lesson_2.5/lambda.k
@@ -1,13 +1,11 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 
-require "substitution.md"
-
 module LAMBDA-SYNTAX
   imports DOMAINS-SYNTAX
-  imports KVAR-SYNTAX
+  imports ID-SYNTAX
 
-  syntax Val ::= KVar
-               | "lambda" KVar "." Exp  [binder]
+  syntax Val ::= Id
+               | "lambda" Id "." Exp
   syntax Exp ::= Val
                | Exp Exp              [left]
                | "(" Exp ")"          [bracket]
@@ -15,7 +13,27 @@ endmodule
 
 module LAMBDA
   imports LAMBDA-SYNTAX
-  imports SUBSTITUTION
+  imports DOMAINS
+
+  syntax Set ::= freeVars( Exp ) [function]
+  rule freeVars( V:Id )         => SetItem(V)
+  rule freeVars( lambda X . E ) => freeVars( E ) -Set SetItem(X)
+  rule freeVars( E1 E2 )        => freeVars(E1) freeVars(E2)
+
+  syntax Id ::= freshVar(Id, Int, Set) [function]
+  rule freshVar(V, I, S) => #let X = String2Id(Id2String(V) +String Int2String(I)) #in #if X in S #then freshVar(V, I +Int 1, S) #else X #fi
+
+  syntax Exp ::= Exp "[" Exp "/" Id "]" [function]
+
+  rule X:Exp [_ / _] => X [owise]
+  rule X [V / X] => V
+
+  rule (lambda Y . E) [_ / Y] => lambda Y . E
+  rule (lambda Y . E) [V / X] => lambda Y . (E[V / X]) requires Y =/=K X andBool notBool (Y in freeVars(V))
+  rule (lambda Y . E) [V / X] => #let Z = freshVar(Y, 0, freeVars(E) freeVars(V)) #in lambda Z . (E[Z / Y] [V / X])
+    requires Y =/=K X andBool Y in freeVars(V)
+
+  rule (E1:Exp E2:Exp) [V / X] => E1[V / X] (E2[V / X])
 
-  rule (lambda X:KVar . E:Exp) V:Val => E[V / X]   [anywhere]
+  rule (lambda X:Id . E:Exp) V:Val => E[V / X]   [anywhere]
 endmodule
diff --git a/1_k/1_lambda/lesson_2/lambda.k b/1_k/1_lambda/lesson_2/lambda.k
index d2227b90..e4306fe9 100644
--- a/1_k/1_lambda/lesson_2/lambda.k
+++ b/1_k/1_lambda/lesson_2/lambda.k
@@ -1,13 +1,11 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 
-require "substitution.md"
-
 module LAMBDA-SYNTAX
   imports DOMAINS-SYNTAX
-  imports KVAR-SYNTAX
+  imports ID-SYNTAX
 
-  syntax Val ::= KVar
-               | "lambda" KVar "." Exp  [binder]
+  syntax Val ::= Id
+               | "lambda" Id "." Exp
   syntax Exp ::= Val
                | Exp Exp              [left]
                | "(" Exp ")"          [bracket]
@@ -15,7 +13,27 @@ endmodule
 
 module LAMBDA
   imports LAMBDA-SYNTAX
-  imports SUBSTITUTION
+  imports DOMAINS
+
+  syntax Set ::= freeVars( Exp ) [function]
+  rule freeVars( V:Id )         => SetItem(V)
+  rule freeVars( lambda X . E ) => freeVars( E ) -Set SetItem(X)
+  rule freeVars( E1 E2 )        => freeVars(E1) freeVars(E2)
+
+  syntax Id ::= freshVar(Id, Int, Set) [function]
+  rule freshVar(V, I, S) => #let X = String2Id(Id2String(V) +String Int2String(I)) #in #if X in S #then freshVar(V, I +Int 1, S) #else X #fi
+
+  syntax Exp ::= Exp "[" Exp "/" Id "]" [function]
+
+  rule X:Exp [_ / _] => X [owise]
+  rule X [V / X] => V
+
+  rule (lambda Y . E) [_ / Y] => lambda Y . E
+  rule (lambda Y . E) [V / X] => lambda Y . (E[V / X]) requires Y =/=K X andBool notBool (Y in freeVars(V))
+  rule (lambda Y . E) [V / X] => #let Z = freshVar(Y, 0, freeVars(E) freeVars(V)) #in lambda Z . (E[Z / Y] [V / X])
+    requires Y =/=K X andBool Y in freeVars(V)
+
+  rule (E1:Exp E2:Exp) [V / X] => E1[V / X] (E2[V / X])
 
-  rule (lambda X:KVar . E:Exp) V:Val => E[V / X]
+  rule (lambda X:Id . E:Exp) V:Val => E[V / X]
 endmodule
diff --git a/1_k/1_lambda/lesson_2/tests/closed-variable-capture.lambda.out b/1_k/1_lambda/lesson_2/tests/closed-variable-capture.lambda.out
index 7cb2c2a2..c79d05f4 100644
--- a/1_k/1_lambda/lesson_2/tests/closed-variable-capture.lambda.out
+++ b/1_k/1_lambda/lesson_2/tests/closed-variable-capture.lambda.out
@@ -1,3 +1,3 @@
 <k>
-  lambda y . ( ( lambda x . lambda y0 . ( x y0 ) ) y ) ~> .
+  lambda y . ( ( lambda x . lambda y . ( x y ) ) y ) ~> .
 </k>
diff --git a/1_k/1_lambda/lesson_2/tests/free-variable-capture.lambda.out b/1_k/1_lambda/lesson_2/tests/free-variable-capture.lambda.out
index 25ced2a2..453eeb2a 100644
--- a/1_k/1_lambda/lesson_2/tests/free-variable-capture.lambda.out
+++ b/1_k/1_lambda/lesson_2/tests/free-variable-capture.lambda.out
@@ -1,3 +1,3 @@
 <k>
-  a ( ( lambda x . lambda y . x ) y0 z ) ~> .
+  a ( ( lambda x . lambda y . x ) y z ) ~> .
 </k>
diff --git a/1_k/1_lambda/lesson_3/lambda.k b/1_k/1_lambda/lesson_3/lambda.k
index 8e4eab88..ceff13db 100644
--- a/1_k/1_lambda/lesson_3/lambda.k
+++ b/1_k/1_lambda/lesson_3/lambda.k
@@ -1,13 +1,11 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 
-require "substitution.md"
-
 module LAMBDA-SYNTAX
   imports DOMAINS-SYNTAX
-  imports KVAR-SYNTAX
+  imports ID-SYNTAX
 
-  syntax Val ::= KVar
-               | "lambda" KVar "." Exp  [binder]
+  syntax Val ::= Id
+               | "lambda" Id "." Exp
   syntax Exp ::= Val
                | Exp Exp              [strict, left]
                | "(" Exp ")"          [bracket]
@@ -15,9 +13,29 @@ endmodule
 
 module LAMBDA
   imports LAMBDA-SYNTAX
-  imports SUBSTITUTION
+  imports DOMAINS
+
+  syntax Set ::= freeVars( Exp ) [function]
+  rule freeVars( V:Id )         => SetItem(V)
+  rule freeVars( lambda X . E ) => freeVars( E ) -Set SetItem(X)
+  rule freeVars( E1 E2 )        => freeVars(E1) freeVars(E2)
+
+  syntax Id ::= freshVar(Id, Int, Set) [function]
+  rule freshVar(V, I, S) => #let X = String2Id(Id2String(V) +String Int2String(I)) #in #if X in S #then freshVar(V, I +Int 1, S) #else X #fi
+
+  syntax Exp ::= Exp "[" Exp "/" Id "]" [function]
+
+  rule X:Exp [_ / _] => X [owise]
+  rule X [V / X] => V
+
+  rule (lambda Y . E) [_ / Y] => lambda Y . E
+  rule (lambda Y . E) [V / X] => lambda Y . (E[V / X]) requires Y =/=K X andBool notBool (Y in freeVars(V))
+  rule (lambda Y . E) [V / X] => #let Z = freshVar(Y, 0, freeVars(E) freeVars(V)) #in lambda Z . (E[Z / Y] [V / X])
+    requires Y =/=K X andBool Y in freeVars(V)
+
+  rule (E1:Exp E2:Exp) [V / X] => E1[V / X] (E2[V / X])
 
   syntax KResult ::= Val
 
-  rule (lambda X:KVar . E:Exp) V:Val => E[V / X]
+  rule (lambda X:Id . E:Exp) V:Val => E[V / X]
 endmodule
diff --git a/1_k/1_lambda/lesson_3/tests/closed-variable-capture.lambda.out b/1_k/1_lambda/lesson_3/tests/closed-variable-capture.lambda.out
index 7cb2c2a2..c79d05f4 100644
--- a/1_k/1_lambda/lesson_3/tests/closed-variable-capture.lambda.out
+++ b/1_k/1_lambda/lesson_3/tests/closed-variable-capture.lambda.out
@@ -1,3 +1,3 @@
 <k>
-  lambda y . ( ( lambda x . lambda y0 . ( x y0 ) ) y ) ~> .
+  lambda y . ( ( lambda x . lambda y . ( x y ) ) y ) ~> .
 </k>
diff --git a/1_k/1_lambda/lesson_4/lambda.k b/1_k/1_lambda/lesson_4/lambda.k
index d92aa528..0872c46e 100644
--- a/1_k/1_lambda/lesson_4/lambda.k
+++ b/1_k/1_lambda/lesson_4/lambda.k
@@ -1,13 +1,11 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 
-require "substitution.md"
-
 module LAMBDA-SYNTAX
   imports DOMAINS-SYNTAX
-  imports KVAR-SYNTAX
+  imports ID-SYNTAX
 
-  syntax Val ::= KVar
-               | "lambda" KVar "." Exp  [binder, latex(\lambda{#1}.{#2})]
+  syntax Val ::= Id
+               | "lambda" Id "." Exp  [latex(\lambda{#1}.{#2})]
   syntax Exp ::= Val
                | Exp Exp              [strict, left]
                | "(" Exp ")"          [bracket]
@@ -15,9 +13,29 @@ endmodule
 
 module LAMBDA
   imports LAMBDA-SYNTAX
-  imports SUBSTITUTION
+  imports DOMAINS
+
+  syntax Set ::= freeVars( Exp ) [function]
+  rule freeVars( V:Id )         => SetItem(V)
+  rule freeVars( lambda X . E ) => freeVars( E ) -Set SetItem(X)
+  rule freeVars( E1 E2 )        => freeVars(E1) freeVars(E2)
+
+  syntax Id ::= freshVar(Id, Int, Set) [function]
+  rule freshVar(V, I, S) => #let X = String2Id(Id2String(V) +String Int2String(I)) #in #if X in S #then freshVar(V, I +Int 1, S) #else X #fi
+
+  syntax Exp ::= Exp "[" Exp "/" Id "]" [function]
+
+  rule X:Exp [_ / _] => X [owise]
+  rule X [V / X] => V
+
+  rule (lambda Y . E) [_ / Y] => lambda Y . E
+  rule (lambda Y . E) [V / X] => lambda Y . (E[V / X]) requires Y =/=K X andBool notBool (Y in freeVars(V))
+  rule (lambda Y . E) [V / X] => #let Z = freshVar(Y, 0, freeVars(E) freeVars(V)) #in lambda Z . (E[Z / Y] [V / X])
+    requires Y =/=K X andBool Y in freeVars(V)
+
+  rule (E1:Exp E2:Exp) [V / X] => E1[V / X] (E2[V / X])
 
   syntax KResult ::= Val
 
-  rule (lambda X:KVar . E:Exp) V:Val => E[V / X]
+  rule (lambda X:Id . E:Exp) V:Val => E[V / X]
 endmodule
diff --git a/1_k/1_lambda/lesson_4/tests/closed-variable-capture.lambda.out b/1_k/1_lambda/lesson_4/tests/closed-variable-capture.lambda.out
index 7cb2c2a2..c79d05f4 100644
--- a/1_k/1_lambda/lesson_4/tests/closed-variable-capture.lambda.out
+++ b/1_k/1_lambda/lesson_4/tests/closed-variable-capture.lambda.out
@@ -1,3 +1,3 @@
 <k>
-  lambda y . ( ( lambda x . lambda y0 . ( x y0 ) ) y ) ~> .
+  lambda y . ( ( lambda x . lambda y . ( x y ) ) y ) ~> .
 </k>
diff --git a/1_k/1_lambda/lesson_5/lambda.k b/1_k/1_lambda/lesson_5/lambda.k
index 786ffb65..dabe6857 100644
--- a/1_k/1_lambda/lesson_5/lambda.k
+++ b/1_k/1_lambda/lesson_5/lambda.k
@@ -1,13 +1,11 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 
-require "substitution.md"
-
 module LAMBDA-SYNTAX
   imports DOMAINS-SYNTAX
-  imports KVAR-SYNTAX
+  imports ID-SYNTAX
 
-  syntax Val ::= KVar
-               | "lambda" KVar "." Exp  [binder, latex(\lambda{#1}.{#2})]
+  syntax Val ::= Id
+               | "lambda" Id "." Exp  [latex(\lambda{#1}.{#2})]
   syntax Exp ::= Val
                | Exp Exp              [strict, left]
                | "(" Exp ")"          [bracket]
@@ -22,12 +20,41 @@ endmodule
 
 module LAMBDA
   imports LAMBDA-SYNTAX
-  imports SUBSTITUTION
   imports DOMAINS
 
+  syntax Set ::= freeVars( Exp ) [function]
+  rule freeVars( _ )            => .Set [owise]
+  rule freeVars( V:Id )         => SetItem(V)
+  rule freeVars( lambda X . E ) => freeVars( E ) -Set SetItem(X)
+  rule freeVars( E1 E2 )        => freeVars(E1) freeVars(E2)
+  rule freeVars( E1 * E2 )      => freeVars(E1) freeVars(E2)
+  rule freeVars( E1 / E2 )      => freeVars(E1) freeVars(E2)
+  rule freeVars( E1 + E2 )      => freeVars(E1) freeVars(E2)
+  rule freeVars( E1 <= E2 )     => freeVars(E1) freeVars(E2)
+
+  syntax Id ::= freshVar(Id, Int, Set) [function]
+  rule freshVar(V, I, S) => #let X = String2Id(Id2String(V) +String Int2String(I)) #in #if X in S #then freshVar(V, I +Int 1, S) #else X #fi
+
+  syntax Exp ::= Exp "[" Exp "/" Id "]" [function]
+
+  rule X:Exp [_ / _] => X [owise]
+  rule X [V / X] => V
+
+  rule (lambda Y . E) [_ / Y] => lambda Y . E
+  rule (lambda Y . E) [V / X] => lambda Y . (E[V / X]) requires Y =/=K X andBool notBool (Y in freeVars(V))
+  rule (lambda Y . E) [V / X] => #let Z = freshVar(Y, 0, freeVars(E) freeVars(V)) #in lambda Z . (E[Z / Y] [V / X])
+    requires Y =/=K X andBool Y in freeVars(V)
+
+  rule (E1:Exp E2:Exp) [V / X] => E1[V / X] (E2[V / X])
+
+  rule (E1:Exp *  E2:Exp) [V / X] => E1[V / X] *  (E2[V / X])
+  rule (E1:Exp /  E2:Exp) [V / X] => E1[V / X] /  (E2[V / X])
+  rule (E1:Exp +  E2:Exp) [V / X] => E1[V / X] +  (E2[V / X])
+  rule (E1:Exp <= E2:Exp) [V / X] => E1[V / X] <= (E2[V / X])
+
   syntax KResult ::= Val
 
-  rule (lambda X:KVar . E:Exp) V:Val => E[V / X]
+  rule (lambda X:Id . E:Exp) V:Val => E[V / X]
 
   rule - I => 0 -Int I
   rule I1 * I2 => I1 *Int I2
diff --git a/1_k/1_lambda/lesson_5/tests/closed-variable-capture.lambda.out b/1_k/1_lambda/lesson_5/tests/closed-variable-capture.lambda.out
index 7cb2c2a2..c79d05f4 100644
--- a/1_k/1_lambda/lesson_5/tests/closed-variable-capture.lambda.out
+++ b/1_k/1_lambda/lesson_5/tests/closed-variable-capture.lambda.out
@@ -1,3 +1,3 @@
 <k>
-  lambda y . ( ( lambda x . lambda y0 . ( x y0 ) ) y ) ~> .
+  lambda y . ( ( lambda x . lambda y . ( x y ) ) y ) ~> .
 </k>
diff --git a/1_k/1_lambda/lesson_6/lambda.k b/1_k/1_lambda/lesson_6/lambda.k
index 01ddcbda..9d955cbf 100644
--- a/1_k/1_lambda/lesson_6/lambda.k
+++ b/1_k/1_lambda/lesson_6/lambda.k
@@ -1,13 +1,11 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 
-require "substitution.md"
-
 module LAMBDA-SYNTAX
   imports DOMAINS-SYNTAX
-  imports KVAR-SYNTAX
+  imports ID-SYNTAX
 
-  syntax Val ::= KVar
-               | "lambda" KVar "." Exp  [binder, latex(\lambda{#1}.{#2})]
+  syntax Val ::= Id
+               | "lambda" Id "." Exp  [latex(\lambda{#1}.{#2})]
   syntax Exp ::= Val
                | Exp Exp              [strict, left]
                | "(" Exp ")"          [bracket]
@@ -24,12 +22,44 @@ endmodule
 
 module LAMBDA
   imports LAMBDA-SYNTAX
-  imports SUBSTITUTION
   imports DOMAINS
 
+  syntax Set ::= freeVars( Exp ) [function]
+  rule freeVars( _ )            => .Set [owise]
+  rule freeVars( V:Id )         => SetItem(V)
+  rule freeVars( lambda X . E ) => freeVars( E ) -Set SetItem(X)
+  rule freeVars( E1 E2 )        => freeVars(E1) freeVars(E2)
+  rule freeVars( E1 * E2 )      => freeVars(E1) freeVars(E2)
+  rule freeVars( E1 / E2 )      => freeVars(E1) freeVars(E2)
+  rule freeVars( E1 + E2 )      => freeVars(E1) freeVars(E2)
+  rule freeVars( E1 <= E2 )     => freeVars(E1) freeVars(E2)
+  rule freeVars( if B then E1 else E2) => freeVars(B) freeVars(E1) freeVars(E2)
+
+  syntax Id ::= freshVar(Id, Int, Set) [function]
+  rule freshVar(V, I, S) => #let X = String2Id(Id2String(V) +String Int2String(I)) #in #if X in S #then freshVar(V, I +Int 1, S) #else X #fi
+
+  syntax Exp ::= Exp "[" Exp "/" Id "]" [function]
+
+  rule X:Exp [_ / _] => X [owise]
+  rule X [V / X] => V
+
+  rule (lambda Y . E) [_ / Y] => lambda Y . E
+  rule (lambda Y . E) [V / X] => lambda Y . (E[V / X]) requires Y =/=K X andBool notBool (Y in freeVars(V))
+  rule (lambda Y . E) [V / X] => #let Z = freshVar(Y, 0, freeVars(E) freeVars(V)) #in lambda Z . (E[Z / Y] [V / X])
+    requires Y =/=K X andBool Y in freeVars(V)
+
+  rule (E1:Exp E2:Exp) [V / X] => E1[V / X] (E2[V / X])
+
+  rule (E1:Exp *  E2:Exp) [V / X] => E1[V / X] *  (E2[V / X])
+  rule (E1:Exp /  E2:Exp) [V / X] => E1[V / X] /  (E2[V / X])
+  rule (E1:Exp +  E2:Exp) [V / X] => E1[V / X] +  (E2[V / X])
+  rule (E1:Exp <= E2:Exp) [V / X] => E1[V / X] <= (E2[V / X])
+
+  rule (if C then E1 else E2) [V / X] => if C[V / X] then E1[V / X] else (E2[V / X])
+
   syntax KResult ::= Val
 
-  rule (lambda X:KVar . E:Exp) V:Val => E[V / X]
+  rule (lambda X:Id . E:Exp) V:Val => E[V / X]
 
   rule - I => 0 -Int I
   rule I1 * I2 => I1 *Int I2
diff --git a/1_k/1_lambda/lesson_6/tests/closed-variable-capture.lambda.out b/1_k/1_lambda/lesson_6/tests/closed-variable-capture.lambda.out
index 7cb2c2a2..c79d05f4 100644
--- a/1_k/1_lambda/lesson_6/tests/closed-variable-capture.lambda.out
+++ b/1_k/1_lambda/lesson_6/tests/closed-variable-capture.lambda.out
@@ -1,3 +1,3 @@
 <k>
-  lambda y . ( ( lambda x . lambda y0 . ( x y0 ) ) y ) ~> .
+  lambda y . ( ( lambda x . lambda y . ( x y ) ) y ) ~> .
 </k>
diff --git a/1_k/1_lambda/lesson_7/lambda.k b/1_k/1_lambda/lesson_7/lambda.k
index 09ae0f90..30d3f4c1 100644
--- a/1_k/1_lambda/lesson_7/lambda.k
+++ b/1_k/1_lambda/lesson_7/lambda.k
@@ -1,13 +1,11 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 
-require "substitution.md"
-
 module LAMBDA-SYNTAX
   imports DOMAINS-SYNTAX
-  imports KVAR-SYNTAX
+  imports ID-SYNTAX
 
-  syntax Val ::= KVar
-               | "lambda" KVar "." Exp  [binder, latex(\lambda{#1}.{#2})]
+  syntax Val ::= Id
+               | "lambda" Id "." Exp  [latex(\lambda{#1}.{#2})]
   syntax Exp ::= Val
                | Exp Exp              [strict, left]
                | "(" Exp ")"          [bracket]
@@ -21,12 +19,12 @@ module LAMBDA-SYNTAX
 
   syntax Exp ::= "if" Exp "then" Exp "else" Exp  [strict(1)]
 
-  syntax Exp ::= "let" KVar "=" Exp "in" Exp [macro]
+  syntax Exp ::= "let" Id "=" Exp "in" Exp [macro]
   rule let X = E in E':Exp => (lambda X . E') E
 
-  syntax Exp ::= "letrec" KVar KVar "=" Exp "in" Exp [macro]
-  syntax KVar ::= "$x" [token] | "$y" [token]
-  rule letrec F:KVar X:KVar = E in E'
+  syntax Exp ::= "letrec" Id Id "=" Exp "in" Exp [macro]
+  syntax Id ::= "$x" [token] | "$y" [token]
+  rule letrec F:Id X:Id = E in E'
     => let F =
          (lambda $x . ((lambda F . lambda X . E) (lambda $y . ($x $x $y))))
          (lambda $x . ((lambda F . lambda X . E) (lambda $y . ($x $x $y))))
@@ -35,12 +33,44 @@ endmodule
 
 module LAMBDA
   imports LAMBDA-SYNTAX
-  imports SUBSTITUTION
   imports DOMAINS
 
+  syntax Set ::= freeVars( Exp ) [function]
+  rule freeVars( _ )            => .Set [owise]
+  rule freeVars( V:Id )         => SetItem(V)
+  rule freeVars( lambda X . E ) => freeVars( E ) -Set SetItem(X)
+  rule freeVars( E1 E2 )        => freeVars(E1) freeVars(E2)
+  rule freeVars( E1 * E2 )      => freeVars(E1) freeVars(E2)
+  rule freeVars( E1 / E2 )      => freeVars(E1) freeVars(E2)
+  rule freeVars( E1 + E2 )      => freeVars(E1) freeVars(E2)
+  rule freeVars( E1 <= E2 )     => freeVars(E1) freeVars(E2)
+  rule freeVars( if B then E1 else E2) => freeVars(B) freeVars(E1) freeVars(E2)
+
+  syntax Id ::= freshVar(Id, Int, Set) [function]
+  rule freshVar(V, I, S) => #let X = String2Id(Id2String(V) +String Int2String(I)) #in #if X in S #then freshVar(V, I +Int 1, S) #else X #fi
+
+  syntax Exp ::= Exp "[" Exp "/" Id "]" [function]
+
+  rule X:Exp [_ / _] => X [owise]
+  rule X [V / X] => V
+
+  rule (lambda Y . E) [_ / Y] => lambda Y . E
+  rule (lambda Y . E) [V / X] => lambda Y . (E[V / X]) requires Y =/=K X andBool notBool (Y in freeVars(V))
+  rule (lambda Y . E) [V / X] => #let Z = freshVar(Y, 0, freeVars(E) freeVars(V)) #in lambda Z . (E[Z / Y] [V / X])
+    requires Y =/=K X andBool Y in freeVars(V)
+
+  rule (E1:Exp E2:Exp) [V / X] => E1[V / X] (E2[V / X])
+
+  rule (E1:Exp *  E2:Exp) [V / X] => E1[V / X] *  (E2[V / X])
+  rule (E1:Exp /  E2:Exp) [V / X] => E1[V / X] /  (E2[V / X])
+  rule (E1:Exp +  E2:Exp) [V / X] => E1[V / X] +  (E2[V / X])
+  rule (E1:Exp <= E2:Exp) [V / X] => E1[V / X] <= (E2[V / X])
+
+  rule (if C then E1 else E2) [V / X] => if C[V / X] then E1[V / X] else (E2[V / X])
+
   syntax KResult ::= Val
 
-  rule (lambda X:KVar . E:Exp) V:Val => E[V / X]
+  rule (lambda X:Id . E:Exp) V:Val => E[V / X]
 
   rule - I => 0 -Int I
   rule I1 * I2 => I1 *Int I2
diff --git a/1_k/1_lambda/lesson_7/tests/closed-variable-capture.lambda.out b/1_k/1_lambda/lesson_7/tests/closed-variable-capture.lambda.out
index 7cb2c2a2..c79d05f4 100644
--- a/1_k/1_lambda/lesson_7/tests/closed-variable-capture.lambda.out
+++ b/1_k/1_lambda/lesson_7/tests/closed-variable-capture.lambda.out
@@ -1,3 +1,3 @@
 <k>
-  lambda y . ( ( lambda x . lambda y0 . ( x y0 ) ) y ) ~> .
+  lambda y . ( ( lambda x . lambda y . ( x y ) ) y ) ~> .
 </k>
diff --git a/1_k/1_lambda/lesson_8/lambda.k b/1_k/1_lambda/lesson_8/lambda.k
index 592fa48d..0f6d5cea 100644
--- a/1_k/1_lambda/lesson_8/lambda.k
+++ b/1_k/1_lambda/lesson_8/lambda.k
@@ -1,13 +1,11 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 
-require "substitution.md"
-
 module LAMBDA-SYNTAX
   imports DOMAINS-SYNTAX
-  imports KVAR-SYNTAX
+  imports ID-SYNTAX
 
-  syntax Val ::= KVar
-               | "lambda" KVar "." Exp  [binder, latex(\lambda{#1}.{#2})]
+  syntax Val ::= Id
+               | "lambda" Id "." Exp  [latex(\lambda{#1}.{#2})]
   syntax Exp ::= Val
                | Exp Exp              [strict, left]
                | "(" Exp ")"          [bracket]
@@ -21,22 +19,54 @@ module LAMBDA-SYNTAX
 
   syntax Exp ::= "if" Exp "then" Exp "else" Exp  [strict(1)]
 
-  syntax Exp ::= "let" KVar "=" Exp "in" Exp [macro]
+  syntax Exp ::= "let" Id "=" Exp "in" Exp [macro]
   rule let X = E in E':Exp => (lambda X . E') E
 
-  syntax Exp ::= "letrec" KVar KVar "=" Exp "in" Exp [macro]
-               | "mu" KVar "." Exp                   [binder, latex(\mu{#1}.{#2})]
-  rule letrec F:KVar X = E in E' => let F = mu F . lambda X . E in E'
+  syntax Exp ::= "letrec" Id Id "=" Exp "in" Exp [macro]
+               | "mu" Id "." Exp                   [latex(\mu{#1}.{#2})]
+  rule letrec F:Id X = E in E' => let F = mu F . lambda X . E in E'
 endmodule
 
 module LAMBDA
   imports LAMBDA-SYNTAX
-  imports SUBSTITUTION
   imports DOMAINS
 
+  syntax Set ::= freeVars( Exp ) [function]
+  rule freeVars( _ )            => .Set [owise]
+  rule freeVars( V:Id )         => SetItem(V)
+  rule freeVars( lambda X . E ) => freeVars( E ) -Set SetItem(X)
+  rule freeVars( E1 E2 )        => freeVars(E1) freeVars(E2)
+  rule freeVars( E1 * E2 )      => freeVars(E1) freeVars(E2)
+  rule freeVars( E1 / E2 )      => freeVars(E1) freeVars(E2)
+  rule freeVars( E1 + E2 )      => freeVars(E1) freeVars(E2)
+  rule freeVars( E1 <= E2 )     => freeVars(E1) freeVars(E2)
+  rule freeVars( if B then E1 else E2) => freeVars(B) freeVars(E1) freeVars(E2)
+
+  syntax Id ::= freshVar(Id, Int, Set) [function]
+  rule freshVar(V, I, S) => #let X = String2Id(Id2String(V) +String Int2String(I)) #in #if X in S #then freshVar(V, I +Int 1, S) #else X #fi
+
+  syntax Exp ::= Exp "[" Exp "/" Id "]" [function]
+
+  rule X:Exp [_ / _] => X [owise]
+  rule X [V / X] => V
+
+  rule (lambda Y . E) [_ / Y] => lambda Y . E
+  rule (lambda Y . E) [V / X] => lambda Y . (E[V / X]) requires Y =/=K X andBool notBool (Y in freeVars(V))
+  rule (lambda Y . E) [V / X] => #let Z = freshVar(Y, 0, freeVars(E) freeVars(V)) #in lambda Z . (E[Z / Y] [V / X])
+    requires Y =/=K X andBool Y in freeVars(V)
+
+  rule (E1:Exp E2:Exp) [V / X] => E1[V / X] (E2[V / X])
+
+  rule (E1:Exp *  E2:Exp) [V / X] => E1[V / X] *  (E2[V / X])
+  rule (E1:Exp /  E2:Exp) [V / X] => E1[V / X] /  (E2[V / X])
+  rule (E1:Exp +  E2:Exp) [V / X] => E1[V / X] +  (E2[V / X])
+  rule (E1:Exp <= E2:Exp) [V / X] => E1[V / X] <= (E2[V / X])
+
+  rule (if C then E1 else E2) [V / X] => if C[V / X] then E1[V / X] else (E2[V / X])
+
   syntax KResult ::= Val
 
-  rule (lambda X:KVar . E:Exp) V:Val => E[V / X]
+  rule (lambda X:Id . E:Exp) V:Val => E[V / X]
 
   rule - I => 0 -Int I
   rule I1 * I2 => I1 *Int I2
diff --git a/1_k/1_lambda/lesson_8/tests/closed-variable-capture.lambda.out b/1_k/1_lambda/lesson_8/tests/closed-variable-capture.lambda.out
index 7cb2c2a2..c79d05f4 100644
--- a/1_k/1_lambda/lesson_8/tests/closed-variable-capture.lambda.out
+++ b/1_k/1_lambda/lesson_8/tests/closed-variable-capture.lambda.out
@@ -1,3 +1,3 @@
 <k>
-  lambda y . ( ( lambda x . lambda y0 . ( x y0 ) ) y ) ~> .
+  lambda y . ( ( lambda x . lambda y . ( x y ) ) y ) ~> .
 </k>
diff --git a/1_k/1_lambda/lesson_9/lambda.md b/1_k/1_lambda/lesson_9/lambda.md
index c3adc750..b8943a60 100644
--- a/1_k/1_lambda/lesson_9/lambda.md
+++ b/1_k/1_lambda/lesson_9/lambda.md
@@ -51,11 +51,9 @@ below.  Then we should make sure we import its module called SUBSTITUTION
 in our LAMBDA module below.
 
 ```k
-require "substitution.md"
-
 module LAMBDA-SYNTAX
   imports DOMAINS-SYNTAX
-  imports KVAR-SYNTAX
+  imports ID-SYNTAX
 ```
 ### Basic Call-by-value λ-Calculus Syntax
 
@@ -77,8 +75,8 @@ interleaved) order.
 
 The initial syntax of our λ-calculus:
 ```k
-  syntax Val ::= KVar
-               | "lambda" KVar "." Exp  [binder, latex(\lambda{#1}.{#2})]
+  syntax Val ::= Id
+               | "lambda" Id "." Exp  [latex(\lambda{#1}.{#2})]
   syntax Exp ::= Val
                | Exp Exp              [left, strict]
                | "(" Exp ")"          [bracket]
@@ -114,7 +112,7 @@ Note that the `if` construct is strict only in its first argument.
 The let binder is a derived construct, because it can be defined using λ.
 
 ```k
-  syntax Exp ::= "let" KVar "=" Exp "in" Exp [macro]
+  syntax Exp ::= "let" Id "=" Exp "in" Exp [macro]
   rule let X = E in E':Exp => (lambda X . E') E
 ```
 
@@ -124,9 +122,9 @@ really necessary, but it makes the definition of letrec easier to understand
 and faster to execute.
 
 ```k
-  syntax Exp ::= "letrec" KVar KVar "=" Exp "in" Exp [macro]
-               | "mu" KVar "." Exp                   [binder, latex(\mu{#1}.{#2})]
-  rule letrec F:KVar X:KVar = E in E' => let F = mu F . lambda X . E in E'
+  syntax Exp ::= "letrec" Id Id "=" Exp "in" Exp [macro]
+               | "mu" Id "." Exp                   [latex(\mu{#1}.{#2})]
+  rule letrec F:Id X:Id = E in E' => let F = mu F . lambda X . E in E'
 endmodule
 ```
 
@@ -135,7 +133,6 @@ endmodule
 ```k
 module LAMBDA
   imports LAMBDA-SYNTAX
-  imports SUBSTITUTION
   imports DOMAINS
 
   syntax KResult ::= Val
@@ -144,7 +141,40 @@ module LAMBDA
 ### β-reduction
 
 ```k
-  rule (lambda X:KVar . E:Exp) V:Val => E[V / X]
+  syntax Set ::= freeVars( Exp ) [function]
+  rule freeVars( _ )            => .Set [owise]
+  rule freeVars( V:Id )         => SetItem(V)
+  rule freeVars( lambda X . E ) => freeVars( E ) -Set SetItem(X)
+  rule freeVars( E1 E2 )        => freeVars(E1) freeVars(E2)
+  rule freeVars( E1 * E2 )      => freeVars(E1) freeVars(E2)
+  rule freeVars( E1 / E2 )      => freeVars(E1) freeVars(E2)
+  rule freeVars( E1 + E2 )      => freeVars(E1) freeVars(E2)
+  rule freeVars( E1 <= E2 )     => freeVars(E1) freeVars(E2)
+  rule freeVars( if B then E1 else E2) => freeVars(B) freeVars(E1) freeVars(E2)
+
+  syntax Id ::= freshVar(Id, Int, Set) [function]
+  rule freshVar(V, I, S) => #let X = String2Id(Id2String(V) +String Int2String(I)) #in #if X in S #then freshVar(V, I +Int 1, S) #else X #fi
+
+  syntax Exp ::= Exp "[" Exp "/" Id "]" [function]
+
+  rule X:Exp [_ / _] => X [owise]
+  rule X [V / X] => V
+
+  rule (lambda Y . E) [_ / Y] => lambda Y . E
+  rule (lambda Y . E) [V / X] => lambda Y . (E[V / X]) requires Y =/=K X andBool notBool (Y in freeVars(V))
+  rule (lambda Y . E) [V / X] => #let Z = freshVar(Y, 0, freeVars(E) freeVars(V)) #in lambda Z . (E[Z / Y] [V / X])
+    requires Y =/=K X andBool Y in freeVars(V)
+
+  rule (E1:Exp E2:Exp) [V / X] => E1[V / X] (E2[V / X])
+
+  rule (E1:Exp *  E2:Exp) [V / X] => E1[V / X] *  (E2[V / X])
+  rule (E1:Exp /  E2:Exp) [V / X] => E1[V / X] /  (E2[V / X])
+  rule (E1:Exp +  E2:Exp) [V / X] => E1[V / X] +  (E2[V / X])
+  rule (E1:Exp <= E2:Exp) [V / X] => E1[V / X] <= (E2[V / X])
+
+  rule (if C then E1 else E2) [V / X] => if C[V / X] then E1[V / X] else (E2[V / X])
+
+  rule (lambda X:Id . E:Exp) V:Val => E[V / X]
 ```
 
 ### Integer Builtins
diff --git a/1_k/1_lambda/lesson_9/tests/closed-variable-capture.lambda.out b/1_k/1_lambda/lesson_9/tests/closed-variable-capture.lambda.out
index 7cb2c2a2..c79d05f4 100644
--- a/1_k/1_lambda/lesson_9/tests/closed-variable-capture.lambda.out
+++ b/1_k/1_lambda/lesson_9/tests/closed-variable-capture.lambda.out
@@ -1,3 +1,3 @@
 <k>
-  lambda y . ( ( lambda x . lambda y0 . ( x y0 ) ) y ) ~> .
+  lambda y . ( ( lambda x . lambda y . ( x y ) ) y ) ~> .
 </k>