diff --git a/SICP_book/chapter_2_2.metta b/SICP_book/chapter_2_2.metta
index 5f67bf7..c59d1a9 100644
--- a/SICP_book/chapter_2_2.metta
+++ b/SICP_book/chapter_2_2.metta
@@ -281,7 +281,8 @@
 
 (: lambda1 (-> Variable Atom (-> $a $t)))
 (= ((lambda1 $var $body) $val)
-    (let (quote $var) (quote $val) $body) )
+  (chain (eval (sealed ($var) ($var $body))) $seal
+    (unify ($sv $sb) $seal (let (quote $sv) (quote $val) $sb) (Error (unify ($sv $sb) $seal) "Unexpected error"))))
 
 (= (square $x)
     (* $x $x))
@@ -573,15 +574,14 @@
 ; Scale tree but using map for definition
 (= (scale-tree-m $tree $factor)
     (map (lambda1 $sub-tree
-        (case $sub-tree
+        (sealed ($_ $x $xs) (case $sub-tree
             (((Cons $x $xs) (scale-tree-m $sub-tree $factor))
-            ($_ (* $sub-tree $factor)))))
+            ($_ (* $sub-tree $factor))))))
             $tree))
 !(assertEqual
     (scale-tree-m (list (1 (list (2 (list (3 4)) 5)) (list (6 7)))) 10)
     (tree (10 (20 (30 40) 50) (60 70))))
 
-
 ; Exercise 2.30.
 ;
 ; Define a procedure square-tree analogous to the square-list procedure
@@ -611,9 +611,9 @@
 
 (= (square-tree-m $tree)
     (map (lambda1 $sub-tree
-        (case $sub-tree
+        (sealed ($_ $x $xs) (case $sub-tree
             (((Cons $x $xs) (square-tree-m $sub-tree))
-            ($_ (* $sub-tree $sub-tree)))))
+            ($_ (* $sub-tree $sub-tree))))))
             $tree))
 
 !(assertEqual
@@ -791,7 +791,8 @@
 
 (: lambda2 (-> Variable Variable Atom (-> $a $b $t)))
 (= ((lambda2 $var1 $var2 $body) $val1 $val2)
-    (let (quote ($var1 $var2)) (quote ($val1 $val2)) $body))
+  (chain (eval (sealed ($var1 $var2) ($var1 $var2 $body))) $seal
+    (unify ($sv1 $sv2 $sb) $seal (let (quote ($sv1 $sv2)) (quote ($val1 $val2)) $sb) (empty)) ))
 
 (= (acc-map $p $sequence)
   (accumulate (lambda2 $x $y (Cons ($p $x) $y)) Nil $sequence))
@@ -983,7 +984,10 @@
 
 (: lambda3 (-> Variable Variable Variable Atom (-> $a $b $c $t)))
 (= ((lambda3 $var1 $var2 $var3 $body) $val1 $val2 $val3)
-    (let (quote ($var1 $var2 $var3)) (quote ($val1 $val2 $val3)) $body))
+  (chain (eval (sealed ($var1 $var2 $var3) ($var1 $var2 $var3 $body))) $seal
+    (unify ($sv1 $sv2 $sv3 $sb) $seal
+       (let (quote ($sv1 $sv2 $sv3)) (quote ($val1 $val2 $val3)) $sb)
+       (Error (unify ($sv1 $sv2 $sv3 $sb) $seal) "Unexpected error"))))
 
 (= (fold-left $op $initial $sequence)
   (let $iter (lambda3 $result $rest $self
@@ -1692,4 +1696,4 @@
 (= (right-split-s) (split beside below))
 (= (up-split-s) (split below beside))
 
-; -----------------------End of Exercise 2.45---------------------------
\ No newline at end of file
+; -----------------------End of Exercise 2.45---------------------------
diff --git a/combinator_logic_experiments/y_comb_examples.metta b/combinator_logic_experiments/y_comb_examples.metta
index 16c583c..63742fb 100644
--- a/combinator_logic_experiments/y_comb_examples.metta
+++ b/combinator_logic_experiments/y_comb_examples.metta
@@ -41,11 +41,11 @@
 ; Non-recursive function defined using Y combinator
 ; Atom type is required type of the first argument otherwise
 ; implementation falls into infinite recursion
-(: id' (-> Atom (-> $t $t)))
-(= ((id' $f) $x) $x)
-(= (id $x) ((Y id') $x))
+(: id'' (-> Atom (-> $t $t)))
+(= ((id'' $f) $x) $x)
+(= (id' $x) ((Y id'') $x))
 
-!(assertEqual (id A) A)
+!(assertEqual (id' A) A)
 
 ; Recursive function defined using Y combinator
 (: fac (-> Atom (-> Int Int)))
@@ -66,12 +66,13 @@
 ; inside let.
 (: lambda (-> Variable Atom (-> Atom $t)))
 (= ((lambda $var $body) $val)
-    (let (quoted $var) (quoted $val) $body))
+  (chain (eval (sealed ($var) ($var $body))) $seal
+    (unify ($sv $sb) $seal (let (quote $sv) (quote $val) $sb) (Error (unify ($sv $sb) $seal ...) "Pair of atoms is expe error"))))
 
 ; Non-recursive function defined using lambda and Y combinator
-(= (id' $x) ((Y (lambda $f (lambda $x $x))) $x))
+(= (id''' $x) ((Y (lambda $f (lambda $x $x))) $x))
 
-!(assertEqual (id' A) A)
+!(assertEqual (id''' A) A)
 
 ; Recursive function defined using lambda and Y combinator
 (= (fact' $y)