diff --git a/model_with_structures/analyzer.ml b/model_with_structures/analyzer.ml
index 6ddc6ad..8c49d32 100644
--- a/model_with_structures/analyzer.ml
+++ b/model_with_structures/analyzer.ml
@@ -438,6 +438,8 @@ struct
     let (mem'', id) = mem_add mem' v in
     (mem'', types_add types x t, vals_add vals x id)
 
+  (* --- *)
+
   let writeval_to_cap (v_w : writeval) : write_cap =
     match v_w with
       | ZeroWV -> NeverWr
@@ -468,29 +470,9 @@ struct
       | RefT (_, t) -> is_all_type_writable t
       | TupleT ts -> List.for_all is_all_type_writable ts
 
-
-  (* - function evaluation *)
-
-  let rec func_eval (state : state) (d : decl) : unit =
-    match d with
-    | FunD (ts, stmt) ->
-      (match state with (mem, types, vals) ->
-       let (state_with_args, _) = List.fold_left
-         (fun (st, x) (m, t) -> (addarg st x t, x + 1))
-         (state, 0) ts in
-    (* NOTE: same x's, so can use same args for all the statements *)
-       match stmt_eval state_with_args stmt with (mem_after_stmt, _, vals_after_stmt) ->
-       ignore @@ List.fold_left
-         (fun x (_, t) ->
-            let id = vals_assoc x vals_after_stmt in
-            let v = mem_get mem_after_stmt id in
-            tags_check mem_after_stmt v t; x + 1)
-         0 ts)
-    | VarD _ -> ()
-
   (* - statement evaluation *)
 
-  and stmt_eval (state : state) (s : stmt) : state =
+  let rec stmt_eval (state : state) (s : stmt) : state =
     match state with (mem, types, vals) -> match s with
     | SkipS -> state
     | CallS (f, es) -> let v = pathval mem vals f in
@@ -530,6 +512,23 @@ struct
                           (* TODO: FIXME: better list union ??  *)
                           else (memcomb meml memr, typesl, valsl)
 
+  (* - function evaluation *)
+
+  let rec func_eval (state : state) (d : decl) : unit =
+    match d with
+    | FunD (ts, stmt) ->
+      (let (state_with_args, _) = List.fold_left
+         (fun (st, x) (m, t) -> (addarg st x t, x + 1))
+         (state, 0) ts in
+       match stmt_eval state_with_args stmt with (mem_after_stmt, _, vals_after_stmt) ->
+       ignore @@ List.fold_left
+         (fun x (_, t) ->
+            let id = vals_assoc x vals_after_stmt in
+            let v = mem_get mem_after_stmt id in
+            tags_check mem_after_stmt v t; x + 1)
+         0 ts)
+    | VarD _ -> ()
+
   (* --- program execution --- *)
 
   let prog_eval (prog : prog) : state =
@@ -610,8 +609,7 @@ struct
 
   let moded t = ((In, NOut), t)
 
-  let defgu t = VarD t
-  let defg t e = VarD t
+  let defg t = VarD t
 
   let wrS p = WriteS p 
   let rdS p = ReadS p 
@@ -712,8 +710,8 @@ struct
   let%expect_test "simple call with read, dsl" =
     prog_eval_noret (
       [
-        defgu uT_r_mw;
-        defg (rfT uT_r_mw) rfg0E;
+        defg uT_r_mw;
+        defg (rfT uT_r_mw);
         FunD (
           [moded @@ cpT @@ uT_r],
           rdS @@ drf @@ v0
@@ -727,8 +725,8 @@ struct
   let%expect_test "simple call with write, dsl" =
     prog_eval_noret (
       [
-        defgu uT_aw;
-        defg (rfT uT_aw) rfg0E;
+        defg uT_aw;
+        defg (rfT uT_aw);
         FunD (
           [moded @@ cpT @@ uT_aw],
           wrS @@ drf @@ v0
@@ -742,8 +740,8 @@ struct
   let%expect_test "simple call with read after write, dsl" =
     prog_eval_noret (
       [
-        defgu uT_aw;
-        defg (rfT uT_aw) rfg0E;
+        defg uT_aw;
+        defg (rfT uT_aw);
         FunD (
           [moded @@ cpT @@ uT_aw],
           (wrS @@ drf @@ v0) #.
@@ -758,8 +756,8 @@ struct
   let%expect_test "simple call with forbidden write, dsl" =
     try (prog_eval_noret (
       [
-        defgu uT_r_mw;
-        defg (rfT uT_r_mw) rfg0E;
+        defg uT_r_mw;
+        defg (rfT uT_r_mw);
         FunD (
           [moded @@ cpT @@ uT_r],
           wrS @@ drf @@ v0
@@ -775,8 +773,8 @@ struct
   let%expect_test "simple call with write to ref, dsl" =
     prog_eval_noret (
       [
-        defgu uT_r_aw;
-        defg (rfT uT_r_aw) rfg0E;
+        defg uT_r_aw;
+        defg (rfT uT_r_aw);
         FunD (
           [moded @@ rfT @@ uT_aw],
           wrS @@ drf @@ v0
@@ -790,8 +788,8 @@ struct
   let%expect_test "simple call with forbidden write to ref, dsl" =
     try (prog_eval_noret (
       [
-        defgu uT_r_aw;
-        defg (rfT uT_r_aw) rfg0E;
+        defg uT_r_aw;
+        defg (rfT uT_r_aw);
         FunD (
           [moded @@ rfT @@ uT_aw],
           wrS @@ drf @@ v0
@@ -807,8 +805,8 @@ struct
   let%expect_test "simple call with write to ref with fix, dsl" =
     prog_eval_noret (
       [
-        defgu uT_r_aw;
-        defg (rfT uT_r_aw) rfg0E;
+        defg uT_r_aw;
+        defg (rfT uT_r_aw);
         FunD (
           [moded @@ rfT @@ uT_aw],
           wrS @@ drf @@ v0
@@ -824,8 +822,8 @@ struct
   let%expect_test "call inside call, dsl" =
     prog_eval_noret (
       [
-        defgu uT_r_aw;
-        defg (rfT uT_r_aw) rfg0E;
+        defg uT_r_aw;
+        defg (rfT uT_r_aw);
         FunD (
           [moded @@ rfT @@ uT_aw],
           wrS @@ drf @@ v0
@@ -846,8 +844,8 @@ struct
   let%expect_test "call inside call, recursive, dsl" =
     prog_eval_noret (
       [
-        defgu uT_r_aw;
-        defg (rfT uT_r_aw) rfg0E;
+        defg uT_r_aw;
+        defg (rfT uT_r_aw);
         FunD (
           [moded @@ cpT @@ uT_aw],
           (callS vg2 [pE v0]) #.
@@ -863,8 +861,8 @@ struct
   let%expect_test "call to fix after call, dsl" =
     prog_eval_noret (
       [
-        defgu uT_r_aw;
-        defg (rfT uT_r_aw) rfg0E;
+        defg uT_r_aw;
+        defg (rfT uT_r_aw);
         FunD (
           [moded @@ rfT @@ uT_aw],
           wrS @@ drf @@ v0
@@ -884,8 +882,8 @@ struct
   let%expect_test "simple call with global variable usage, dsl" =
     prog_eval_noret (
       [
-        defgu uT_r_aw;
-        defg (rfT uT_r) rfg0E;
+        defg uT_r_aw;
+        defg (rfT uT_r);
         FunD (
           [moded @@ cpT @@ uT],
           (wrS @@ vg0) #.
@@ -901,10 +899,10 @@ struct
   let%expect_test "simple call with read & write (2 args), dsl" =
     prog_eval_noret (
       [
-        defgu uT_r;
-        defg (rfT uT_r) rfg0E;
-        defgu uT_aw;
-        defg (rfT uT_aw) rfg2E;
+        defg uT_r;
+        defg (rfT uT_r);
+        defg uT_aw;
+        defg (rfT uT_aw);
         FunD (
           [
             moded @@ rfT @@ uT_r;
@@ -922,14 +920,14 @@ struct
   let%expect_test "simple call with different arguments modifiers, copy, dsl" =
     prog_eval_noret (
       [
-        defgu uT_r_aw;
-        defg (rfT uT_r_aw) rfg0E;
-        defgu uT_r_aw;
-        defg (rfT uT_r_aw) rfg2E;
-        defgu uT_r_aw;
-        defg (rfT uT_r_aw) rfg4E;
-        defgu uT_r_aw;
-        defg (rfT uT_r_aw) rfg6E;
+        defg uT_r_aw;
+        defg (rfT uT_r_aw);
+        defg uT_r_aw;
+        defg (rfT uT_r_aw);
+        defg uT_r_aw;
+        defg (rfT uT_r_aw);
+        defg uT_r_aw;
+        defg (rfT uT_r_aw);
         FunD (
           [
             ((NIn, NOut), cpT @@ uT);
@@ -956,14 +954,14 @@ struct
   let%expect_test "simple call with different arguments modifiers, ref, dsl" =
     prog_eval_noret (
       [
-        defgu uT_r;
-        defg (rfT uT_r) rfg0E;
-        defgu uT_r;
-        defg (rfT uT_r) rfg2E;
-        defgu uT_r_aw;
-        defg (rfT uT_r_aw) rfg4E;
-        defgu uT_r_aw;
-        defg (rfT uT_r_aw) rfg6E;
+        defg uT_r;
+        defg (rfT uT_r);
+        defg uT_r;
+        defg (rfT uT_r);
+        defg uT_r_aw;
+        defg (rfT uT_r_aw);
+        defg uT_r_aw;
+        defg (rfT uT_r_aw);
         FunD (
           [
             ((NIn, NOut), rfT @@ uT);
@@ -991,14 +989,14 @@ struct
   let%expect_test "presentation test 1 (simple types), dsl" =
     prog_eval_noret (
       [
-        defgu uT_r_aw;
-        defg (rfT uT_r_aw) rfg0E; (* x *)
-        defgu uT_r_aw;
-        defg (rfT uT_r_aw) rfg2E; (* y *)
-        defgu uT_r_aw;
-        defg (rfT uT_r_aw) rfg4E; (* z *)
-        defgu uT_r_aw;
-        defg (rfT uT_r_aw) rfg6E; (* k *)
+        defg uT_r_aw;
+        defg (rfT uT_r_aw); (* x *)
+        defg uT_r_aw;
+        defg (rfT uT_r_aw); (* y *)
+        defg uT_r_aw;
+        defg (rfT uT_r_aw); (* z *)
+        defg uT_r_aw;
+        defg (rfT uT_r_aw); (* k *)
         FunD ( (* f *)
           [
             (moded @@ rfT @@ uT_r_aw);
@@ -1069,7 +1067,7 @@ struct
       (* [ *)
         (* defg userT userE; *)
         (* defg dataT dataE; *)
-        (* defgu uT_r_aw; (* time *) *)
+        (* defg uT_r_aw; (* time *) *)
         (* defg requestT requestE; *)
         (* FunD ( (* send *) *)
           (* [ *)
@@ -1164,7 +1162,7 @@ struct
         (* defg userT userE; *)
         (* defg versionT versionE; *)
         (* defg utilsT utilsE; *)
-        (* defgu uT_r_aw; *)
+        (* defg uT_r_aw; *)
         (* defg requestT requestE; *)
         (* get_version_idF; *)
         (* updated_versionF; *)
diff --git a/model_with_structures/model.typ b/model_with_structures/model.typ
index bc169ac..887e5bf 100644
--- a/model_with_structures/model.typ
+++ b/model_with_structures/model.typ
@@ -1118,7 +1118,7 @@ $action$ - действия, совершаемые с примитивным з
     // NOTE: expr type expected to ~ match t (maybe except some automaticc modifiers)
     // expect well typed program
 
-    $cl mu cr xarrowSquiggly(t)_build cl v, mu' cr$, // TODO: FIXME check (required?)
+    $cl mu cr xarrowSquiggly(t)_build cl v, mu' cr$,
     $mu' xarrowSquiggly(v)_#[add] cl l, mu'' cr$,
 
     $cl types, vals, mu cr xarrowSquiggly("var" x : t)_init cl types[x <- t], vals[x <- l], mu'' cr$
@@ -1516,6 +1516,8 @@ $action$ - действия, совершаемые с примитивным з
   )
 ))
 
+#h(10pt)
+
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
diff --git a/model_with_structures/synthesizer.ml b/model_with_structures/synthesizer.ml
index 2d699bc..8987412 100644
--- a/model_with_structures/synthesizer.ml
+++ b/model_with_structures/synthesizer.ml
@@ -147,7 +147,7 @@ struct
   module Decl = struct
     [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
     [%%ocanren_inject
-      type nonrec ((* 'd, *) 't, 'e, (* 'dl, *) 'mtl, 's) t = VarD of (* 'd * *) 't * 'e | FunD of (* 'd * 'dl * *) 'mtl * 's
+      type nonrec ((* 'd, *) 't, 'e, (* 'dl, *) 'mtl, 's) t = VarD of (* 'd * *) 't | FunD of (* 'd * 'dl * *) 'mtl * 's
       [@@deriving gt ~options:{ show; gmap }]
       type ground = ((* Nat.ground, *) Type.ground, Expr.ground, (* Nat.ground List.ground, *) (Mode.ground * Type.ground) List.ground, Stmt.ground) t
     ]
@@ -194,13 +194,12 @@ struct
   module Value = struct
     [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
     [%%ocanren_inject
-      type nonrec ('vm, 'vr, 'vw, 'sl, 'd, 'vl) t = UnitV of 'vm * 'vr * 'vw
-                                                  | FunV of 'sl
-                                                  | RefV of 'd
-                                                  | TupleV of 'vl
+      type nonrec ('vm, 'vr, 'vw, 'd, 'vl) t = UnitV of 'vm * 'vr * 'vw
+                                             | FunV
+                                             | RefV of 'd
+                                             | TupleV of 'vl
       [@@deriving gt ~options:{ show; gmap }]
       type ground = (MemVal.ground, ReadVal.ground, WriteVal.ground,
-                     ((* Nat.ground List.ground * *) Stmt.ground) List.ground,
                      Nat.ground, ground List.ground) t
     ]
   end
@@ -237,7 +236,7 @@ struct
   module TypesEnv = struct
     [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
     [%%ocanren_inject
-      type nonrec 'dtl t = TypesEnv of 'dtl (* glob *) * 'dtl (* glob + loc *)
+      type nonrec 'dtl t = TypesEnv of 'dtl
       [@@deriving gt ~options:{ show; gmap }]
       type nonrec ground = ((Nat.ground * Type.ground) List.ground) t
     ]
@@ -246,27 +245,18 @@ struct
   module ValsEnv = struct
     [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
     [%%ocanren_inject
-      type nonrec 'ddl t = ValsEnv of 'ddl (* glob *) * 'ddl (* glob + loc *)
+      type nonrec 'ddl t = ValsEnv of 'ddl
       [@@deriving gt ~options:{ show; gmap }]
       type nonrec ground = ((Nat.ground * Nat.ground) List.ground) t
     ]
   end
 
-  module VisitedEnv = struct
-    [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
-    [%%ocanren_inject
-      type nonrec 'sl t = VisitedEnv of 'sl
-      [@@deriving gt ~options:{ show; gmap }]
-      type nonrec ground = (Stmt.ground List.ground) t
-    ]
-  end
-
   module StEnv = struct
     [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
     [%%ocanren_inject
-      type nonrec ('mem, 'types, 'vals, 'visited) t = StEnv of 'mem * 'types * 'vals * 'visited
+      type nonrec ('mem, 'types, 'vals) t = StEnv of 'mem * 'types * 'vals
       [@@deriving gt ~options:{ show; gmap }]
-      type nonrec ground = (MemEnv.ground, TypesEnv.ground, ValsEnv.ground, VisitedEnv.ground) t
+      type nonrec ground = (MemEnv.ground, TypesEnv.ground, ValsEnv.ground) t
     ]
   end
 
@@ -405,87 +395,35 @@ struct
   let types_assoco id types tp =
     let open TypesEnv in
     ocanren {
-      fresh _glob_tps, tps in
-      types == TypesEnv (_glob_tps, tps) &
+      fresh tps in
+      types == TypesEnv tps &
       List.assoco id tps tp
     }
 
   let vals_assoco id vals v =
     let open ValsEnv in
     ocanren {
-      fresh _glob_vs, vs in
-      vals == ValsEnv (_glob_vs, vs) &
+      fresh vs in
+      vals == ValsEnv vs &
       List.assoco id vs v
     }
 
-  let types_glob_addo types x tp types' = 
-    let open TypesEnv in
-    ocanren {
-      fresh glob_tps, tps in
-      types == TypesEnv (glob_tps, tps) &
-      types' == TypesEnv ((Std.pair x tp) :: glob_tps,
-                          (Std.pair x tp) :: tps)
-  }
-
   let types_addo types x tp types' = 
     let open TypesEnv in
     ocanren {
-      fresh glob_tps, tps in
-      types == TypesEnv (glob_tps, tps) &
-      types' == TypesEnv (glob_tps, (Std.pair x tp) :: tps)
-  }
-
-  let vals_glob_addo vals x v vals' = 
-    let open ValsEnv in
-    ocanren {
-      fresh glob_vs, vs in
-      vals == ValsEnv (glob_vs, vs) &
-      vals' == ValsEnv ((Std.pair x v) :: glob_vs,
-                        (Std.pair x v) :: vs)
+      fresh tps in
+      types == TypesEnv tps &
+      types' == TypesEnv ((Std.pair x tp) :: tps)
   }
 
   let vals_addo vals x v vals' = 
     let open ValsEnv in
     ocanren {
-      fresh glob_vs, vs in
-      vals == ValsEnv (glob_vs, vs) &
-      vals' == ValsEnv (glob_vs, (Std.pair x v) :: vs)
+      fresh vs in
+      vals == ValsEnv vs &
+      vals' == ValsEnv ((Std.pair x v) :: vs)
   }
 
-  let visited_appendo visitedl visitedr visited' = 
-    let open VisitedEnv in
-    ocanren {
-      fresh vsl, vsr, vs' in
-      visitedl == VisitedEnv vsl &
-      visitedr == VisitedEnv vsr &
-      List.appendo vsl vsr vs' &
-      visited' == VisitedEnv vs'
-  }
-
-  let visited_checko visited stmt =
-    let open VisitedEnv in
-    ocanren {
-      fresh vs in
-      visited == VisitedEnv vs &
-      List.membero vs stmt
-    }
-
-  let not_visited_checko visited stmt =
-    let open VisitedEnv in
-    ocanren {
-      fresh vs in
-      visited == VisitedEnv vs &
-      list_not_membero vs stmt
-    }
-
-  let visited_addo visited stmt visited' =
-    let open VisitedEnv in
-    ocanren {
-      fresh vs in
-      visited == VisitedEnv vs &
-      visited' == VisitedEnv (stmt :: vs)
-    }
-
   (* --- *)
 
   let mem_geto mem id v =
@@ -626,51 +564,51 @@ struct
         mem_with_id' == Std.pair mem' (TupleV vs') }
   }
 
-  let rec valcopy_foldero mem_with_vs v tp mem_with_vs' =
-    ocanren {
-      fresh mem, vs, mem', v', vs' in
-      Std.pair mem vs == mem_with_vs &
-      valcopyo mem v tp (Std.pair mem' v') &
-      vs' == v' :: vs &
-      mem_with_vs' == Std.pair mem' vs'
-  }
-  and valcopyo mem v tp mem_with_id' = 
-    let open Type in
-    let open Value in
-    let open ReadCap in
+  (* let rec valcopy_foldero mem_with_vs v tp mem_with_vs' = *)
+    (* ocanren { *)
+      (* fresh mem, vs, mem', v', vs' in *)
+      (* Std.pair mem vs == mem_with_vs & *)
+      (* valcopyo mem v tp (Std.pair mem' v') & *)
+      (* vs' == v' :: vs & *)
+      (* mem_with_vs' == Std.pair mem' vs' *)
+  (* } *)
+  (* and valcopyo mem v tp mem_with_id' = *) 
+    (* let open Type in *)
+    (* let open Value in *)
+    (* let open ReadCap in *)
     (* let open CopyCap in *)
-    let open MemVal in
-    let open ReadVal in
-    let open WriteVal in
-    ocanren {
-      { fresh r, w in
-        tp == UnitT (r, w) &
-        { { fresh v_m, _v_r, _v_w in
-            r == Rd &
-            v == UnitV (v_m, _v_r, _v_w) &
-            mem_with_id' == Std.pair mem (UnitV (v_m, ZeroRV, ZeroWV)) } |
-          { r == NRd &
-            mem_with_id' == Std.pair mem (UnitV (BotMV, ZeroRV, ZeroWV)) } } } |
-      { fresh stmts, ts in
-        v == FunV stmts &
-        tp == FunT ts &
-        mem_with_id' == Std.pair mem v } |
-      { fresh c, tp', id in
-        v == RefV id &
-        tp == RefT (c, tp') &
+    (* let open MemVal in *)
+    (* let open ReadVal in *)
+    (* let open WriteVal in *)
+    (* ocanren { *)
+      (* { fresh r, w in *)
+        (* tp == UnitT (r, w) & *)
+        (* { { fresh v_m, _v_r, _v_w in *)
+            (* r == Rd & *)
+            (* v == UnitV (v_m, _v_r, _v_w) & *)
+            (* mem_with_id' == Std.pair mem (UnitV (v_m, ZeroRV, ZeroWV)) } | *)
+          (* { r == NRd & *)
+            (* mem_with_id' == Std.pair mem (UnitV (BotMV, ZeroRV, ZeroWV)) } } } | *)
+      (* { fresh stmts, ts in *)
+        (* v == FunV stmts & *)
+        (* tp == FunT ts & *)
+        (* mem_with_id' == Std.pair mem v } | *)
+      (* { fresh c, tp', id in *)
+        (* v == RefV id & *)
+        (* tp == RefT (c, tp') & *)
         (* { c == Rf & mem_with_id' == Std.pair mem v } | *)
-        { fresh v', mem_cp, v_cp, mem_add, id_add in
+        (* { fresh v', mem_cp, v_cp, mem_add, id_add in *)
           (* c == Cp & *)
-          mem_geto mem id v' &
-          valcopyo mem v' tp' (Std.pair mem_cp v_cp) &
-          mem_addo mem_cp v_cp (Std.pair mem_add id_add) &
-          mem_with_id' == (mem_add, RefV id_add) } } |
-      { fresh vs, tps, mem', vs' in
-        v == TupleV vs &
-        tp == TupleT tps &
-        list_foldr2o valcopy_foldero (Std.pair mem []) vs tps (Std.pair mem' vs') &
-        mem_with_id' == Std.pair mem' (TupleV vs') }
-  }
+          (* mem_geto mem id v' & *)
+          (* valcopyo mem v' tp' (Std.pair mem_cp v_cp) & *)
+          (* mem_addo mem_cp v_cp (Std.pair mem_add id_add) & *)
+          (* mem_with_id' == (mem_add, RefV id_add) } } | *)
+      (* { fresh vs, tps, mem', vs' in *)
+        (* v == TupleV vs & *)
+        (* tp == TupleT tps & *)
+        (* list_foldr2o valcopy_foldero (Std.pair mem []) vs tps (Std.pair mem' vs') & *)
+        (* mem_with_id' == Std.pair mem' (TupleV vs') } *)
+  (* } *)
 
   (* - action rules *)
 
@@ -820,12 +758,9 @@ struct
       readvalcombo u_r v_r u_r' &
       writevalcombo u_w v_w u_w' &
       u' == UnitV (u_m', u_r', u_w') } |
-    { fresh ustmts, vstmts, ustmts' in
-      u == FunV ustmts &
-      v == FunV vstmts &
-      (* TODO: swap stmts order o efficiency ? *)
-      List.appendo ustmts vstmts ustmts' &
-      u' == FunV ustmts' } |
+    { u == FunV &
+      v == FunV &
+      u' == FunV } |
     { fresh a, b in
       u == RefV a &
       v == RefV b &
@@ -910,32 +845,26 @@ struct
     let open Value in
     let open Type in
     ocanren {
-      fresh mem, types, vals, visited in
-      st == StEnv (mem, types, vals, visited) &
+      fresh mem, types, vals in
+      st == StEnv (mem, types, vals) &
       {
-        { fresh tp, e, v,
-                mem_cp, v_cp,
+        { fresh tp, mem_bd, v_bd,
                 mem_add, id_add,
                 types', vals' in
-          d == VarD (tp, e) &
-          exprvalo mem vals e v &
-          valcopyo mem v tp (Pair.pair mem_cp v_cp) &
-          (* mem_cp == mem & v_cp == v & *)
-          mem_addo mem_cp v_cp (Pair.pair mem_add id_add) &
-          (* mem_add == mem_cp & *)
-          types_glob_addo types x tp types' &
-          (* types == types' & *)
-          (* vals == vals' & *)
-          vals_glob_addo vals x id_add vals' &
-          st' == StEnv (mem_add, types', vals', visited) } |
+          d == VarD tp &
+          valbuildo mem tp (Pair.pair mem_bd v_bd) &
+          mem_addo mem_bd v_bd (Pair.pair mem_add id_add) &
+          types_addo types x tp types' &
+          vals_addo vals x id_add vals' &
+          st' == StEnv (mem_add, types', vals') } |
         { fresh tps, s,
                 mem_add, id_add,
                 types', vals' in
           d == FunD (tps, s) &
-          mem_addo mem (FunV [s]) (Pair.pair mem_add id_add) &
-          types_glob_addo types x (FunT tps) types' &
-          vals_glob_addo vals x id_add vals' &
-          st' == StEnv (mem_add, types', vals', visited)
+          mem_addo mem FunV (Pair.pair mem_add id_add) &
+          types_addo types x (FunT tps) types' &
+          vals_addo vals x id_add vals' &
+          st' == StEnv (mem_add, types', vals')
          }
       }
   }
@@ -948,11 +877,10 @@ struct
     let open StEnv in
     let open TypesEnv in
     let open ValsEnv in
-    let open VisitedEnv in
     ocanren {
       fresh m in
       empty_memo m &
-      st == StEnv (m, TypesEnv ([], []), ValsEnv ([], []), VisitedEnv [])
+      st == StEnv (m, TypesEnv [], ValsEnv [])
   }
 
   (* TODO: better way ??? *)
@@ -1058,9 +986,9 @@ struct
             v'' == UnitV (v_m''', v_r'', v_w'') &
             mem_with_v' == Std.pair mem v'' }
         } } |
-      { fresh ts, _stmts in
+      { fresh ts in
         tp == FunT ts &
-        v == FunV _stmts &
+        v == FunV &
         mem_with_v' == Std.pair mem v } |
       { fresh ctp', tp', id', v', mem_sp, v_sp, mem_set in
         tp == RefT (ctp', tp') &
@@ -1086,10 +1014,10 @@ struct
     let open CopyCap in
     let open RevPath in
     ocanren {
-      fresh mem, types, vals, visited,
+      fresh mem, types, vals,
             x, id, b(* , tp' *), rp,
             mem_sp, b_sp, v_sp, mem_upd, v_upd in
-      st == StEnv (mem, types, vals, visited) &
+      st == StEnv (mem, types, vals) &
       pathvaro p x &
       vals_assoco x vals id &
       pathvalo mem vals p b &
@@ -1101,11 +1029,11 @@ struct
       mem_seto mem_upd id v_upd mem'
   }
 
-  let rec argsspoile_foldero types vals visited m mem tp e mem' =
+  let rec argsspoile_foldero types vals m mem tp e mem' =
     let open StEnv in
     ocanren {
       fresh st in
-      st == StEnv (mem, types, vals, visited) &
+      st == StEnv (mem, types, vals) &
       argsspoileo st m tp e mem'
   }
   and argsspoileo st m tp e mem' =
@@ -1114,8 +1042,8 @@ struct
     let open Type in
     let open Path in
     ocanren {
-      fresh _r, _w, mem, types, vals, visited in
-      st == StEnv (mem, types, vals, visited) &
+      fresh _r, _w, mem, types, vals in
+      st == StEnv (mem, types, vals) &
       {
         { e == UnitE &
           tp == UnitT (_r, _w) &
@@ -1129,30 +1057,28 @@ struct
         { fresh es, tps in
           e == TupleE es &
           tp == TupleT tps &
-          list_foldl2o (argsspoile_foldero types vals visited m) mem tps es mem'}
+          list_foldl2o (argsspoile_foldero types vals m) mem tps es mem'}
       }
   }
 
   (* - funciton argument addition *)
 
-  let addargo st oldvals x tp e st' =
+  let addargo st x tp st' =
     let open StEnv in
     ocanren {
-      fresh mem, types, vals, visited, v,
-            mem_cp, v_cp,
+      fresh mem, types, vals,
+            mem_bd, v_bd,
             mem_add, id_add,
             types', vals' in
-      st == StEnv (mem, types, vals, visited) &
-      exprvalo mem oldvals e v &
-      valcopyo mem v tp (Std.pair mem_cp v_cp) &
-      mem_addo mem_cp v_cp (Std.pair mem_add id_add) &
+      st == StEnv (mem, types, vals) &
+      valbuildo mem tp (Std.pair mem_bd v_bd) &
+      mem_addo mem_bd v_bd (Std.pair mem_add id_add) &
       types_addo types x tp types' &
       vals_addo vals x id_add vals' &
-      st' == StEnv (mem_add, types', vals', visited)
+      st' == StEnv (mem_add, types', vals')
   }
 
-  (* - function evaluation *)
-  (* NOTE: not needed due to performed optimization in stmt_eval ? *)
+  (* --- *)
 
   let writeval_to_capo v_w w' =
     let open WriteVal in
@@ -1180,8 +1106,8 @@ struct
         } &
         writeval_to_capo v_w w
          } |
-      { fresh _stmts, _ts in
-        v == FunV _stmts &
+      { fresh _ts in
+        v == FunV &
         tp == FunT _ts } |
       { fresh id, _c, tp', v' in
         v == RefV id &
@@ -1215,90 +1141,34 @@ struct
 
   (* - statement evaluation *)
 
-  let rec stmt_addarg_foldero vals st_with_id mtp e st_with_id' = ocanren {
-    fresh st, x, m, tp, st' in
-    Std.pair st x == st_with_id &
-    Std.pair m tp == mtp &
-    addargo st vals x tp e st' &
-    st_with_id' == Std.pair st' (Nat.s x)
-  }
-  and f_tags_check_foldero mem vals x mtp x' = ocanren {
-    fresh m, tp, id', v' in
-    mtp == Std.pair m tp &
-    vals_assoco x vals id' &
-    mem_geto mem id' v' &
-    tags_checko mem v' tp &
-    x' == Nat.s x
-  }
-  and stmt_eval_func_foldero mem types vals tps visited stmt visited' =
-    let open StEnv in
-    ocanren {
-      { fresh visited_add, st,
-              st', mem', types', vals',
-              _x', visited'' in
-        not_visited_checko visited stmt &
-        visited_addo visited stmt visited_add &
-        st == StEnv (mem, types, vals, visited_add) &
-        stmt_evalo st stmt st' &
-        st' == StEnv (mem', types', vals', visited'') &
-        list_foldlo (f_tags_check_foldero mem' vals') 0 tps _x' &
-        visited' == visited''
-         } |
-      { visited_checko visited stmt &
-        visited == visited' }
-  }
-  and stmt_eval_spoil_foldero types vals visited mem mtp e mem' =
+  let rec stmt_eval_spoil_foldero types vals mem mtp e mem' =
     let open StEnv in
     ocanren {
       fresh m, tp, st in
       Std.pair m tp == mtp &
-      st == StEnv (mem, types, vals, visited) &
+      st == StEnv (mem, types, vals) &
       argsspoileo st m tp e mem'
   }
   and stmt_evalo st s st' =
     let open StEnv in
     let open Stmt in
-    let open Value in
     let open Type in
-    (* let open WriteCap in *)
-    let open TypesEnv in
-    let open ValsEnv in
     let open RevPath in
     let open Action in
     ocanren {
-      fresh mem, types, vals, visited in
-      st == StEnv (mem, types, vals, visited) &
+      fresh mem, types, vals in
+      st == StEnv (mem, types, vals) &
       {
         { s == SkipS & st == st' } |
-        { fresh f, es, v, tp,
-                glob_tps, _tps,
-                glob_vs, _vs,
-                types_call, vals_call,
-                fstmts, tps, st_call,
-                state_with_args,
-                mem_swa, types_swa,
-                vals_swa, visited_swa,
-                _arg_id, mem_spoiled,
-                visited' in
+        { fresh f, es, tp,
+                _tps, _vs, tps,
+                mem_spoiled in
           s == CallS (f, es) &
-          pathvalo mem vals f v &
           pathtypeo types f tp &
-          types == TypesEnv (glob_tps, _tps) &
-          vals == ValsEnv (glob_vs, _vs) &
-          types_call == TypesEnv (glob_tps, glob_tps) &
-          vals_call == ValsEnv (glob_vs, glob_vs) &
-          v == FunV fstmts &
           tp == FunT tps &
-          st_call == StEnv (mem, types_call, vals_call, visited) &
-          list_foldl2o (stmt_addarg_foldero vals)
-                       (Std.pair st_call 0) tps es
-                       (Std.pair state_with_args _arg_id) &
-          state_with_args == StEnv (mem_swa, types_swa, vals_swa, visited_swa) &
-          list_foldlo (stmt_eval_func_foldero mem_swa types_swa vals_swa tps) visited_swa fstmts visited' &
-          (* TODO: FIXME check left or right order *)
-          list_foldl2o (stmt_eval_spoil_foldero types vals (* NOTE: not important*) visited')
+          list_foldl2o (stmt_eval_spoil_foldero types vals)
                        mem tps es mem_spoiled &
-          st' == StEnv (mem_spoiled, types, vals, visited')
+          st' == StEnv (mem_spoiled, types, vals)
         } |
         { fresh p, tp, x, id, v, rp,
                 mem_upd, v_upd, mem_set in
@@ -1311,7 +1181,7 @@ struct
           pathrevo p VarRP rp &
           valupdo mem v rp AlwaysWriteA (Std.pair mem_upd v_upd) &
           mem_seto mem_upd id v_upd mem_set &
-          st' == StEnv (mem_set, types, vals, visited) } |
+          st' == StEnv (mem_set, types, vals) } |
         { fresh p, _tp, _r, _w, x, id, v, rp,
                 mem_upd, v_upd, mem_set in
           s == ReadS p &
@@ -1321,7 +1191,7 @@ struct
           pathrevo p VarRP rp &
           valupdo mem v rp ReadA (Std.pair mem_upd v_upd) &
           mem_seto mem_upd id v_upd mem_set &
-          st' == StEnv (mem_set, types, vals, visited) } |
+          st' == StEnv (mem_set, types, vals) } |
         (* { fresh p in *)
           (* s == ReadS p & *)
           (* pathvalo mem vals p ZeroV & *)
@@ -1331,22 +1201,58 @@ struct
           stmt_evalo st sl stl &
           stmt_evalo stl sr st' } |
         { fresh sl, sr, stl, str,
-                meml, typesl, valsl, visitedl,
-                memr, typesr, valsr, visitedr,
-                visited', mem' in
+                meml, typesl, valsl,
+                memr, typesr, valsr,
+                mem' in
           s == ChoiceS (sl, sr) &
           stmt_evalo st sl stl &
           stmt_evalo st sr str &
-          stl == StEnv (meml, typesl, valsl, visitedl) &
-          str == StEnv (memr, typesr, valsr, visitedr) &
+          stl == StEnv (meml, typesl, valsl) &
+          str == StEnv (memr, typesr, valsr) &
           typesl == typesr &
           valsl == valsr &
           memcombo meml memr mem' &
-          visited_appendo visitedr visitedl visited' &
-          st' == StEnv (mem', typesl, valsl, visited') }
+          st' == StEnv (mem', typesl, valsl) }
       }
   }
 
+  (* - function evaluation *)
+
+  let rec f_addarg_foldero st_with_id mtp st_with_id' = ocanren {
+    fresh st, x, m, tp, st' in
+    Std.pair st x == st_with_id &
+    Std.pair m tp == mtp &
+    addargo st x tp st' &
+    st_with_id' == Std.pair st' (Nat.s x)
+  }
+  and f_tags_check_foldero mem vals x mtp x' = ocanren {
+    fresh m, tp, id', v' in
+    mtp == Std.pair m tp &
+    vals_assoco x vals id' &
+    mem_geto mem id' v' &
+    tags_checko mem v' tp &
+    x' == Nat.s x
+  }
+
+  (* list_foldlo (stmt_eval_func_foldero mem_swa types_swa vals_swa tps) visited_swa fstmts visited' & *)
+  and func_evalo st d =
+    let open StEnv in
+    let open Decl in
+    ocanren {
+      { fresh tps, stmt,
+              state_with_args, _arg_id, st_after_stmt,
+              mem_after_stmt, _types_after_stmt, vals_after_stmt, _x' in
+        d == FunD (tps, stmt) &
+        list_foldlo f_addarg_foldero
+                    (Std.pair st 0) tps
+                    (Std.pair state_with_args _arg_id) &
+        stmt_evalo state_with_args stmt st_after_stmt &
+        state_with_args == StEnv (mem_after_stmt, _types_after_stmt, vals_after_stmt) &
+        list_foldlo (f_tags_check_foldero mem_after_stmt vals_after_stmt) 0 tps _x'
+         } |
+      { fresh _tp in
+        d == VarD _tp }
+  }
   (* --- program execution --- *)
 
   let prog_evalo prog st' =
@@ -1355,6 +1261,7 @@ struct
       fresh decls, s, init_st in
       prog == Prg (decls, s) &
       prog_inito prog init_st &
+      list_checko (func_evalo init_st) decls &
       stmt_evalo init_st s st'
   }
 end
diff --git a/model_with_structures/tests.ml b/model_with_structures/tests.ml
index 5433e74..fe16bd6 100644
--- a/model_with_structures/tests.ml
+++ b/model_with_structures/tests.ml
@@ -5,19 +5,19 @@ open Relational
   (* - basic var tests *)
 
 let%expect_test "prog eval test: empty" = print_endline (prog_eval_t_empty ());
-  [%expect {| [StEnv (MemEnv ([], O), TypesEnv ([], []), ValsEnv ([], []), VisitedEnv ([]))] |}]
+  [%expect {| [StEnv (MemEnv ([], O), TypesEnv ([]), ValsEnv ([]))] |}]
 let%expect_test "prog eval test: simple var" = print_endline(prog_eval_t_simple_var ());
-  [%expect {| [StEnv (MemEnv ([UnitV (ZeroMV, OneRV, ZeroWV)], S (O)), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, MayWr))], [(S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, MayWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (O)))))))))), O)], [(S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]), VisitedEnv ([]))] |}]
+  [%expect {| [StEnv (MemEnv ([UnitV (ZeroMV, OneRV, ZeroWV)], S (O)), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (Rd, MayWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]))] |}]
 let%expect_test "simple var, forbidden read" = print_endline(prog_eval_t_simple_var_fbd_rd ());
   [%expect {| [] |}]
 let%expect_test "simple vars, no read & read" = print_endline(prog_eval_t_simple_vars_fbd_rd_rd ());
-  [%expect {| [StEnv (MemEnv ([UnitV (ZeroMV, OneRV, ZeroWV); UnitV (BotMV, ZeroRV, ZeroWV)], S (S (O))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (O))))))))))), UnitT (Rd, MayWr)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (NRd, MayWr))], [(S (S (S (S (S (S (S (S (S (S (S (O))))))))))), UnitT (Rd, MayWr)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (NRd, MayWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)], [(S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]), VisitedEnv ([]))] |}]
+  [%expect {| [StEnv (MemEnv ([UnitV (ZeroMV, OneRV, ZeroWV); UnitV (BotMV, ZeroRV, ZeroWV)], S (S (O))), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (S (O))))))))))), UnitT (Rd, MayWr)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (NRd, MayWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (S (O))))))))))), S (O)); (S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]))] |}]
 let%expect_test "simple var, write" = print_endline(prog_eval_t_simple_var_wr ());
-  [%expect {| [StEnv (MemEnv ([UnitV (ZeroMV, TopRV, OneWV)], S (O)), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (NRd, MayWr))], [(S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (NRd, MayWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (O)))))))))), O)], [(S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]), VisitedEnv ([]))] |}]
+  [%expect {| [StEnv (MemEnv ([UnitV (ZeroMV, TopRV, OneWV)], S (O)), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (NRd, MayWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]))] |}]
 let%expect_test "simple var, forbidden write" = print_endline(prog_eval_t_simple_var_fbd_wr ());
   [%expect {| [] |}]
 let%expect_test "simple var, write & read" = print_endline(prog_eval_t_simple_var_wr_rd ());
-  [%expect {| [StEnv (MemEnv ([UnitV (ZeroMV, TopRV, OneWV)], S (O)), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (NRd, MayWr))], [(S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (NRd, MayWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (O)))))))))), O)], [(S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]), VisitedEnv ([]))] |}]
+  [%expect {| [StEnv (MemEnv ([UnitV (ZeroMV, TopRV, OneWV)], S (O)), TypesEnv ([(S (S (S (S (S (S (S (S (S (S (O)))))))))), UnitT (NRd, MayWr))]), ValsEnv ([(S (S (S (S (S (S (S (S (S (S (O)))))))))), O)]))] |}]
 
   (* - basic call tests *)
 
diff --git a/model_with_structures/tests_f.ml b/model_with_structures/tests_f.ml
index 6f65938..24a39eb 100644
--- a/model_with_structures/tests_f.ml
+++ b/model_with_structures/tests_f.ml
@@ -67,7 +67,7 @@ let prog_eval_t_simple_var _ = show(answer) (Stream.take (run q
   (fun q -> ocanren {
               fresh prog, xg in
               globals_min_ido xg &
-              prog == Prg ([VarD (UnitT (Rd, MayWr), UnitE)],
+              prog == Prg ([VarD (UnitT (Rd, MayWr))],
                            ReadS (VarP xg)) &
               prog_evalo prog q })
   (fun q -> q#reify (StEnv.prj_exn))))
@@ -87,7 +87,7 @@ let prog_eval_t_simple_var_fbd_rd _ = show(answer) (Stream.take (run q
   (fun q -> ocanren {
               fresh prog, xg in
               globals_min_ido xg &
-              prog == Prg ([VarD (UnitT (NRd, MayWr), UnitE)],
+              prog == Prg ([VarD (UnitT (NRd, MayWr))],
                            ReadS (VarP xg)) &
               prog_evalo prog q })
   (fun q -> q#reify (StEnv.prj_exn))))
@@ -97,8 +97,8 @@ let prog_eval_t_simple_vars_fbd_rd_rd _ = show(answer) (Stream.take (run q
               fresh prog, xg, yg in
               globals_min_ido xg &
               yg == Nat.s xg &
-              prog == Prg ([VarD (UnitT (NRd, MayWr), UnitE);
-                            VarD (UnitT (Rd, MayWr), UnitE)],
+              prog == Prg ([VarD (UnitT (NRd, MayWr));
+                            VarD (UnitT (Rd, MayWr))],
                            ReadS (VarP yg)) &
               prog_evalo prog q })
   (fun q -> q#reify (StEnv.prj_exn))))
@@ -107,7 +107,7 @@ let prog_eval_t_simple_var_wr _ = show(answer) (Stream.take (run q
   (fun q -> ocanren {
               fresh prog, xg in
               globals_min_ido xg &
-              prog == Prg ([VarD (UnitT (NRd, MayWr), UnitE)],
+              prog == Prg ([VarD (UnitT (NRd, MayWr))],
                            WriteS (VarP xg)) &
               prog_evalo prog q })
   (fun q -> q#reify (StEnv.prj_exn))))
@@ -116,7 +116,7 @@ let prog_eval_t_simple_var_fbd_wr _ = show(answer) (Stream.take (run q
   (fun q -> ocanren {
               fresh prog, xg in
               globals_min_ido xg &
-              prog == Prg ([VarD (UnitT (NRd, NeverWr), UnitE)],
+              prog == Prg ([VarD (UnitT (NRd, NeverWr))],
                            WriteS (VarP xg)) &
               prog_evalo prog q })
   (fun q -> q#reify (StEnv.prj_exn))))
@@ -125,7 +125,7 @@ let prog_eval_t_simple_var_wr_rd _ = show(answer) (Stream.take (run q
   (fun q -> ocanren {
               fresh prog, xg in
               globals_min_ido xg &
-              prog == Prg ([VarD (UnitT (NRd, MayWr), UnitE)],
+              prog == Prg ([VarD (UnitT (NRd, MayWr))],
                            SeqS (WriteS (VarP xg),
                                  ReadS (VarP xg))) &
               prog_evalo prog q })
@@ -139,7 +139,7 @@ let prog_eval_t_simple_var_wr_rd _ = show(answer) (Stream.take (run q
               (* fresh prog, xg, fg, xd, fd in *)
               (* globals_min_ido xg & *)
               (* fg == Nat.s xg & *)
-              (* xd == VarD (UnitT (Rd, NeverWr), UnitE) & *)
+              (* xd == VarD (UnitT (Rd, NeverWr)) & *)
               (* fd == FunD ([], SkipS) & *)
               (* prog == Prg ([xd; fd], CallS (VarP fg, [])) & *)
               (* prog_evalo prog q }) *)
@@ -150,7 +150,7 @@ let prog_eval_t_simple_call_rd _ = show(answer) (Stream.take (run q
               fresh prog, xg, fg, xd, fd in
               globals_min_ido xg &
               fg == Nat.s xg &
-              xd == VarD (UnitT (Rd, NeverWr), UnitE) &
+              xd == VarD (UnitT (Rd, NeverWr)) &
               fd == FunD ([(Mode (In, NOut), UnitT (Rd, NeverWr))], ReadS (VarP 0)) &
               prog == Prg ([xd; fd], CallS (VarP fg, [PathE (VarP xg)])) &
               prog_evalo prog q })
@@ -162,8 +162,8 @@ let prog_eval_t_simple_call_rd_ref _ = show(answer) (Stream.take (run q
               globals_min_ido xg &
               yg == Nat.s xg &
               fg == Nat.s yg &
-              xd == VarD (UnitT (Rd, NeverWr), UnitE) &
-              yd == VarD (RefT (Rf, UnitT (Rd, NeverWr)), RefE xg) &
+              xd == VarD (UnitT (Rd, NeverWr)) &
+              yd == VarD (RefT (Rf, UnitT (Rd, NeverWr))) &
               fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, NeverWr)))],
                           ReadS (DerefP (VarP 0))) &
               prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) &
@@ -176,8 +176,8 @@ let prog_eval_t_simple_call_wr _ = show(answer) (Stream.take (run q
               globals_min_ido xg &
               yg == Nat.s xg &
               fg == Nat.s yg &
-              xd == VarD (UnitT (NRd, AlwaysWr), UnitE) &
-              yd == VarD (RefT (Rf, UnitT (NRd, AlwaysWr)), RefE xg) &
+              xd == VarD (UnitT (NRd, AlwaysWr)) &
+              yd == VarD (RefT (Rf, UnitT (NRd, AlwaysWr))) &
               fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))],
                           WriteS (DerefP (VarP 0))) &
               prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) &
@@ -190,8 +190,8 @@ let prog_eval_t_simple_call_wr_rd _ = show(answer) (Stream.take (run q
               globals_min_ido xg &
               yg == Nat.s xg &
               fg == Nat.s yg &
-              xd == VarD (UnitT (NRd, MayWr), UnitE) &
-              yd == VarD (RefT (Rf, UnitT (NRd, MayWr)), RefE xg) &
+              xd == VarD (UnitT (NRd, MayWr)) &
+              yd == VarD (RefT (Rf, UnitT (NRd, MayWr))) &
               fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))],
                           SeqS (WriteS (DerefP (VarP 0)),
                                 ReadS (DerefP (VarP 0)))) &
@@ -205,8 +205,8 @@ let prog_eval_t_simple_call_fbd_wr _ = show(answer) (Stream.take (run q
               globals_min_ido xg &
               yg == Nat.s xg &
               fg == Nat.s yg &
-              xd == VarD (UnitT (Rd, MayWr), UnitE) &
-              yd == VarD (RefT (Rf, UnitT (Rd, MayWr)), RefE xg) &
+              xd == VarD (UnitT (Rd, MayWr)) &
+              yd == VarD (RefT (Rf, UnitT (Rd, MayWr))) &
               fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, NeverWr)))],
                           WriteS (DerefP (VarP 0))) &
               prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) &
@@ -219,8 +219,8 @@ let prog_eval_t_simple_call_ref_wr _ = show(answer) (Stream.take (run q
               globals_min_ido xg &
               yg == Nat.s xg &
               fg == Nat.s yg &
-              xd == VarD (UnitT (NRd, AlwaysWr), UnitE) &
-              yd == VarD (RefT (Rf, UnitT (NRd, AlwaysWr)), RefE xg) &
+              xd == VarD (UnitT (NRd, AlwaysWr)) &
+              yd == VarD (RefT (Rf, UnitT (NRd, AlwaysWr))) &
               fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))],
                           WriteS (DerefP (VarP 0))) &
               prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) &
@@ -233,8 +233,8 @@ let prog_eval_t_simple_call_ref_fbd_wr _ = show(answer) (Stream.take (run q
               globals_min_ido xg &
               yg == Nat.s xg &
               fg == Nat.s yg &
-              xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
-              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
+              xd == VarD (UnitT (Rd, AlwaysWr)) &
+              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
               fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr)))],
                           WriteS (DerefP (VarP 0))) &
               prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]),
@@ -248,8 +248,8 @@ let prog_eval_t_simple_call_ref_wr_with_fix _ = show(answer) (Stream.take (run q
               globals_min_ido xg &
               yg == Nat.s xg &
               fg == Nat.s yg &
-              xd == VarD (UnitT (NRd, AlwaysWr), UnitE) &
-              yd == VarD (RefT (Rf, UnitT (NRd, AlwaysWr)), RefE xg) &
+              xd == VarD (UnitT (NRd, AlwaysWr)) &
+              yd == VarD (RefT (Rf, UnitT (NRd, AlwaysWr))) &
               fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))],
                           WriteS (DerefP (VarP 0))) &
               prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]),
@@ -265,8 +265,8 @@ let prog_eval_t_call_in_call _ = show(answer) (Stream.take (run q
               yg == Nat.s xg &
               fg == Nat.s yg &
               f2g == Nat.s fg &
-              xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
-              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
+              xd == VarD (UnitT (Rd, AlwaysWr)) &
+              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
               fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))],
                           WriteS (DerefP (VarP 0))) &
               f2d == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))],
@@ -283,8 +283,8 @@ let prog_eval_t_call_in_call_rec _ = show(answer) (Stream.take (run q
               globals_min_ido xg &
               yg == Nat.s xg &
               fg == Nat.s yg &
-              xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
-              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
+              xd == VarD (UnitT (Rd, AlwaysWr)) &
+              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
               fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))],
                           SeqS (CallS (VarP fg, [PathE (VarP 0)]),
                                 WriteS (DerefP (VarP 0)))) &
@@ -300,8 +300,8 @@ let prog_eval_t_fix_call_after_call _ = show(answer) (Stream.take (run q
               yg == Nat.s xg &
               fg == Nat.s yg &
               f2g == Nat.s fg &
-              xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
-              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
+              xd == VarD (UnitT (Rd, AlwaysWr)) &
+              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
               fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))],
                           WriteS (DerefP (VarP 0))) &
               f2d == FunD ([(Mode (In, Out), RefT (Rf, UnitT (NRd, AlwaysWr)))],
@@ -318,8 +318,8 @@ let prog_eval_t_call_with_glob_usage _ = show(answer) (Stream.take (run q
               globals_min_ido xg &
               yg == Nat.s xg &
               fg == Nat.s yg &
-              xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
-              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
+              xd == VarD (UnitT (Rd, AlwaysWr)) &
+              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
               fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, NeverWr)))],
                           SeqS (WriteS (VarP xg),
                                 ReadS (DerefP (VarP 0)))) &
@@ -337,10 +337,10 @@ let prog_eval_t_call_with_rd_wr_2_args _ = show(answer) (Stream.take (run q
               x2g == Nat.s yg &
               y2g == Nat.s x2g &
               fg == Nat.s y2g &
-              xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
-              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
-              x2d == VarD (UnitT (Rd, AlwaysWr), UnitE) &
-              y2d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE x2g) &
+              xd == VarD (UnitT (Rd, AlwaysWr)) &
+              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
+              x2d == VarD (UnitT (Rd, AlwaysWr)) &
+              y2d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
               fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr)));
                            (Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))],
                           SeqS (ReadS (DerefP (VarP 0)),
@@ -375,14 +375,14 @@ let prog_eval_t_call_with_dif_mods_cp _ = show(answer) (Stream.take (run q
               x4g == Nat.s y3g &
               y4g == Nat.s x4g &
               fg == Nat.s y4g &
-              xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
-              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
-              x2d == VarD (UnitT (Rd, AlwaysWr), UnitE) &
-              y2d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE x2g) &
-              x3d == VarD (UnitT (Rd, AlwaysWr), UnitE) &
-              y3d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE x3g) &
-              x4d == VarD (UnitT (Rd, AlwaysWr), UnitE) &
-              y4d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE x4g) &
+              xd == VarD (UnitT (Rd, AlwaysWr)) &
+              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
+              x2d == VarD (UnitT (Rd, AlwaysWr)) &
+              y2d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
+              x3d == VarD (UnitT (Rd, AlwaysWr)) &
+              y3d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
+              x4d == VarD (UnitT (Rd, AlwaysWr)) &
+              y4d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
               seqo [ReadS (DerefP (VarP 1));
                     ReadS (DerefP (VarP 3));
                     WriteS (DerefP (VarP 1));
@@ -434,14 +434,14 @@ let prog_eval_t_call_with_dif_mods_rf _ = show(answer) (Stream.take (run q
               x4g == Nat.s y3g &
               y4g == Nat.s x4g &
               fg == Nat.s y4g &
-              xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
-              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
-              x2d == VarD (UnitT (Rd, AlwaysWr), UnitE) &
-              y2d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE x2g) &
-              x3d == VarD (UnitT (Rd, AlwaysWr), UnitE) &
-              y3d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE x3g) &
-              x4d == VarD (UnitT (Rd, AlwaysWr), UnitE) &
-              y4d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE x4g) &
+              xd == VarD (UnitT (Rd, AlwaysWr)) &
+              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
+              x2d == VarD (UnitT (Rd, AlwaysWr)) &
+              y2d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
+              x3d == VarD (UnitT (Rd, AlwaysWr)) &
+              y3d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
+              x4d == VarD (UnitT (Rd, AlwaysWr)) &
+              y4d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
               seqo [ReadS (DerefP (VarP 1));
                     ReadS (DerefP (VarP 3));
                     WriteS (DerefP (VarP 2));
@@ -477,8 +477,8 @@ let prog_cp_cap_synt_t_simple_call_ref_wr _ = show(answerCpCap) (Stream.take (ru
               globals_min_ido xg &
               yg == Nat.s xg &
               fg == Nat.s yg &
-              xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
-              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
+              xd == VarD (UnitT (Rd, AlwaysWr)) &
+              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
               fd == FunD ([(Mode (In, NOut), RefT (q, UnitT (NRd, AlwaysWr)))],
                           WriteS (DerefP (VarP 0))) &
               prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) &
@@ -492,8 +492,8 @@ let prog_cp_cap_synt_t_simple_call_ref_wr' _ = show(answerCpCap) (Stream.take (r
               globals_min_ido xg &
               yg == Nat.s xg &
               fg == Nat.s yg &
-              xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
-              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
+              xd == VarD (UnitT (Rd, AlwaysWr)) &
+              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
               fd == FunD ([(Mode (In, NOut), RefT (q, UnitT (rd_cap, wr_cap)))],
                           WriteS (DerefP (VarP 0))) &
               prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) &
@@ -506,8 +506,8 @@ let prog_cp_cap_synt_t_simple_call_ref_fbd_wr _ = show(answerCpCap) (Stream.take
               globals_min_ido xg &
               yg == Nat.s xg &
               fg == Nat.s yg &
-              xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
-              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
+              xd == VarD (UnitT (Rd, AlwaysWr)) &
+              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
               fd == FunD ([(Mode (In, NOut), RefT (q, UnitT (NRd, AlwaysWr)))],
                           WriteS (DerefP (VarP 0))) &
               prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]),
@@ -522,8 +522,8 @@ let prog_cp_cap_synt_t_simple_call_ref_fbd_wr' _ = show(answerCpCap) (Stream.tak
               globals_min_ido xg &
               yg == Nat.s xg &
               fg == Nat.s yg &
-              xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
-              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
+              xd == VarD (UnitT (Rd, AlwaysWr)) &
+              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
               fd == FunD ([(Mode (In, NOut), RefT (q, UnitT (rd_cap, wr_cap)))],
                           WriteS (DerefP (VarP 0))) &
               prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]),
@@ -561,14 +561,14 @@ let prog_eval_t_presentation_simple_tp _ = show(answer) (Stream.take (run q
               wg == Nat.s fg &
               gg == Nat.s wg &
               rg == Nat.s gg &
-              xbd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
-              xd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xbg) &
-              ybd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
-              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE ybg) &
-              zbd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
-              zd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE zbg) &
-              kbd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
-              kd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE kbg) &
+              xbd == VarD (UnitT (Rd, AlwaysWr)) &
+              xd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
+              ybd == VarD (UnitT (Rd, AlwaysWr)) &
+              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
+              zbd == VarD (UnitT (Rd, AlwaysWr)) &
+              zd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
+              kbd == VarD (UnitT (Rd, AlwaysWr)) &
+              kd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
               seqo [ReadS (DerefP (VarP 0));
                     WriteS (DerefP (VarP 0));
                     ReadS (DerefP (VarP 1))] fstmts &
@@ -635,14 +635,14 @@ let prog_synt_t_presentation_simple_tp _ = show(answerCpCapList) (Stream.take (r
               wg == Nat.s fg &
               gg == Nat.s wg &
               rg == Nat.s gg &
-              xbd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
-              xd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xbg) &
-              ybd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
-              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE ybg) &
-              zbd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
-              zd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE zbg) &
-              kbd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
-              kd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE kbg) &
+              xbd == VarD (UnitT (Rd, AlwaysWr)) &
+              xd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
+              ybd == VarD (UnitT (Rd, AlwaysWr)) &
+              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
+              zbd == VarD (UnitT (Rd, AlwaysWr)) &
+              zd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
+              kbd == VarD (UnitT (Rd, AlwaysWr)) &
+              kd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
               seqo [ReadS (DerefP (VarP 0));
                     WriteS (DerefP (VarP 0));
                     ReadS (DerefP (VarP 1))] fstmts &
@@ -828,10 +828,10 @@ let prog_eval_t_presentation_complex_tp _ = show(answer) (Stream.take (run q
                     ReadS time_gp
                   ] stmts &
               prog == Prg ([
-                            VarD (userT, userE);
-                            VarD (dataT, dataE);
-                            VarD (timeT, timeE);
-                            VarD (requestT, requestE);
+                            VarD userT;
+                            VarD dataT;
+                            VarD timeT;
+                            VarD requestT;
                             sendD
                             ],
                            stmts
@@ -898,10 +898,10 @@ let prog_synt_t_presentation_complex_tp _ = show(answerCpCapList) (Stream.take (
                     ReadS time_gp
                   ] stmts &
               prog == Prg ([
-                            VarD (userT, userE);
-                            VarD (dataT, dataE);
-                            VarD (timeT, timeE);
-                            VarD (requestT, requestE);
+                            VarD userT;
+                            VarD dataT;
+                            VarD timeT;
+                            VarD requestT;
                             sendD
                             ],
                            stmts
@@ -1041,13 +1041,13 @@ let prog_eval_compl_test_send _ = show(answer) (Stream.take (run q
                    send_allF &
 
               prog == Prg ([
-                VarD (user_utilsT, user_utilsE);
-                VarD (user_infoT, user_infoE);
-                VarD (userT, userE);
-                VarD (versionT, versionE);
-                VarD (utilsT, utilsE);
-                VarD (uT_r_aw, UnitE); (* data *)
-                VarD (requestT, requestE);
+                VarD user_utilsT;
+                VarD user_infoT;
+                VarD userT;
+                VarD versionT;
+                VarD utilsT;
+                VarD uT_r_aw; (* data *)
+                VarD requestT;
                 FunD ([moded_requestT], get_version_idF);
                 FunD ([moded_requestT], updated_versionF);
                 FunD ([moded_requestT], sendF);
@@ -1336,13 +1336,13 @@ let prog_synt_compl_test_send _ = show(answerCpCapList) (Stream.take (run q
               (* [gvi_c0; gvi_c1; gvi_c2; gvi_c3; gvi_c4; gvi_c5] & *)
 
               prog == Prg ([
-                VarD (user_utilsT, user_utilsE);
-                VarD (user_infoT, user_infoE);
-                VarD (userT, userE);
-                VarD (versionT, versionE);
-                VarD (utilsT, utilsE);
-                VarD (uT_r_aw, UnitE); (* data *)
-                VarD (requestT, requestE);
+                VarD user_utilsT;
+                VarD user_infoT;
+                VarD userT;
+                VarD versionT;
+                VarD utilsT;
+                VarD uT_r_aw; (* data *)
+                VarD requestT;
                 (* FunD ([mrT'], get_version_idF); *)
                 (* FunD ([mrT'], updated_versionF); *)
                 (* FunD ([mrT'], sendF); *)