diff --git a/model_with_structures/analyzer.ml b/model_with_structures/analyzer.ml
index 3e8ec19..006a42a 100644
--- a/model_with_structures/analyzer.ml
+++ b/model_with_structures/analyzer.ml
@@ -27,8 +27,7 @@ struct
 
   type expr = UnitE
             | PathE of path
-            (* TODO: extend to include arbitrary path *)
-            | RefE of data
+            (* | RefE *)
             | TupleE of expr list
 
   type stmt = SkipS
@@ -97,11 +96,11 @@ struct
     (* (((snd mem, v) :: fst mem, snd mem + 1), snd mem) *)
   (* let mem_set (mem : mem) (id : memid) (v : value) : mem = *)
     (* ((id, v) :: fst mem, snd mem) *)
-  let mem_get (mem : mem) (id : memid) : value = (* FIXME TMP Printf.printf "l%i i%i %i: access\n" (snd mem) id (snd mem - id - 1); *) List.nth (fst mem) (snd mem - id - 1)
+  let mem_get (mem : mem) (id : memid) : value = List.nth (fst mem) id
   let mem_add (mem : mem) (v : value) : mem * memid =
     ((v :: fst mem, snd mem + 1), snd mem)
   let mem_set (mem : mem) (id : memid) (v : value) : mem =
-    (list_replace (fst mem) (snd mem - id - 1) v, snd mem)
+    (list_replace (fst mem) id v, snd mem)
 
   let rec v_to_deepv (mem : mem) (v : value) : deepvalue = match v with
     | ZeroV -> ZeroDV
@@ -131,12 +130,7 @@ struct
                            | _ -> raise @@ Typing_error "pathtype: access"
 
   let rec pathval (mem :  mem) (vals : vals) (p : path) : value = match p with
-    | VarP x -> mem_get mem @@ ((* Printf.printf "%i: " x; (* FIXME TMP *)
-                                ignore @@ List.map (fun (x, _) -> Printf.printf "%i " x) vals;
-                                Printf.printf "mem size: %i, " (List.length (fst mem));
-                                Printf.printf "mem size stored: %i " (snd mem);
-                                Printf.printf "\n"; *)
-                                List.assoc x vals)
+    | VarP x -> mem_get mem @@ List.assoc x vals
     | DerefP p -> (match pathval mem vals p with
                     | RefV id -> mem_get mem id
                     | _ -> raise @@ Typing_error "pathval: deref")
@@ -203,7 +197,6 @@ struct
   let rec exprval (mem : mem) (vals : vals) (e : expr) : value = match e with
     | UnitE -> ZeroV
     | PathE p -> pathval mem vals p
-    | RefE x -> RefV (List.assoc x vals)
     | TupleE es -> TupleV (List.map (exprval mem vals) es)
 
   (* - expression typing *)
@@ -211,7 +204,6 @@ struct
   let rec exprtype (types : types) (e : expr) : atype = match e with
     | UnitE -> UnitT (Rd, NeverWr)
     | PathE p -> pathtype types p
-    | RefE x -> RefT (Rf, List.assoc x types)
     | TupleE es -> TupleT (List.map (exprtype types) es)
 
   (* - context initialization *)
@@ -228,8 +220,7 @@ struct
     | FunD (ts, s)  -> let (mem', id) = mem_add mem (FunV [s]) in
                        (mem', (x, FunT ts) :: types, (x, id) :: vals)
 
-  let empty_mem : mem = ([], 0)
-  let empty_state : state = (empty_mem, [], [])
+  let empty_state : state = (([], 0), [], [])
 
   (* TODO: better way ??? *)
   let globals_min_id : data = 1000
@@ -246,18 +237,11 @@ struct
   let is_correct_tags (v : value) (r : read_cap) (w : write_cap)
                       (r' : read_cap) (w' : write_cap) (m : mode)
                       (c : copy_cap) : bool =
-    (* FIXME TMP
-    Printf.printf "%b %b %b %b %b\n"
-      (r != Rd || v == ZeroV)
-      (r != Rd || fst m == In)
-      (snd m != Out || w == AlwaysWr)
-      (((not @@ (w == AlwaysWr || w == MayWr) && (snd m == Out || c == Rf)) || w' == AlwaysWr))
-      (is_trivial_v v); *)
     (r != Rd || v == ZeroV) &&
     (r != Rd || fst m == In) &&
     (snd m != Out || w == AlwaysWr) &&
     (* TODO: check *)
-    ((not ((w == AlwaysWr || w == MayWr) && (snd m == Out || c == Rf))) || w' == AlwaysWr) &&
+    ((not @@ (w == AlwaysWr || w == MayWr) && (snd m == Out || c == Rf)) || w' == AlwaysWr) &&
     is_trivial_v v
 
   let rec valspoil (mem : mem) (v : value) (t : atype)
@@ -307,13 +291,13 @@ struct
 
   (* - funciton argument addition *)
 
-  let addarg (state : state) (oldvals : vals) (x : data) (t : atype) (e : expr) : state =
+  let addarg (state : state) (x : data) (t : atype) (e : expr) : state =
     match state with (mem, types, vals) ->
-    let v = exprval mem oldvals e in
+    let v = exprval mem vals e in
     (* let t' = pathtype types p in *)
     let (mem', v') = valcopy mem v t in
     let (mem'', id) = mem_add mem' v in
-    (mem'', (x, t) :: types, (x, id) :: vals)
+    (mem', (x, t) :: types, (x, id) :: vals)
 
   (* - function evaluation *)
 
@@ -326,25 +310,23 @@ struct
     match state with (mem, types, vals) -> match s with
     (* TODO: FIXME: Add memoisation *)
     | SkipS -> state
-    | CallS (f, es) -> let v = (* FIXME TMP Printf.printf "call, before v\n"; *) pathval mem vals f in
-                       let t = (* FIXME TMP Printf.printf "call, before t\n"; *) pathtype types f in
+    | CallS (f, es) -> let v = pathval mem vals f in
+                       let t = pathtype types f in
                        let types' : types = [] in
                        let vals' : vals = [] in
                        (match v, t with
                           | FunV (* xs, *) fstmts (* ) *), FunT ts ->
                             (* TODO: memoisation of the called functions *)
-                            let (state_with_args, _) = (* FIXME TMP Printf.printf "call, before args\n"; *) List.fold_left2 (* TODO: FIXME: check x's order *)
-                              (fun (st, x) (m, t) p -> (addarg st vals x t p, x + 1))
+                            let (state_with_args, _) = List.fold_left2 (* TODO: FIXME: check x's order *)
+                              (fun (st, x) (m, t) p -> (addarg st x t p, x + 1))
                               ((mem, types', vals'), 0) ts es in
                             (* NOTE: same x's, so can use same args for all the statements *)
-                            let _states_evaled = (* FIXME TMP Printf.printf "call, before eval\n"; *) List.map (stmt_eval state_with_args) fstmts in
-                            let mem_spoiled = (* FIXME TMP Printf.printf "call, before spoil\n"; *) List.fold_left2
+                            let _states_evaled = List.map (stmt_eval state_with_args) fstmts in
+                            let mem_spoiled = List.fold_left2
                               (fun mem (m, t) e -> argsspoile (mem, types, vals) m t e)
                               mem ts es in
                             (mem_spoiled, types, vals)
-                          | FunV _, _ -> raise @@ Eval_error "call: function type"
-                          | _, FunT _ -> raise @@ Eval_error "call: function val"
-                          | _, _ -> raise @@ Eval_error "call: function type & val")
+                          | _, _ -> raise @@ Eval_error "call: function")
     | WriteS p -> (match pathtype types p with
                      | UnitT (_, w) ->
                        if w == NeverWr
@@ -379,59 +361,7 @@ struct
 
   (* --- tests --- *)
 
-  (* - shortcuts *)
-
-  let ( #. ) x y = SeqS (x, y)
-
-  let vx = VarP 0
-  let vy = VarP 1
-  let vz = VarP 2
-
-  let vgx = VarP (globals_min_id)
-  let vgy = VarP (globals_min_id + 1)
-  let vgz = VarP (globals_min_id + 2)
-
-  let drf p = DerefP p
-  let access p i = AccessP (p, i)
-
-  let wr x = ReadS x 
-  let rd x = WriteS x
-  let skp = SkipS
-
-  let uT_r_aw = UnitT (Rd, AlwaysWr)
-  let uT_r_mw = UnitT (Rd, MayWr)
-  let uT_aw = UnitT (NRd, AlwaysWr)
-  let uT_mw = UnitT (NRd, MayWr)
-  let uT_r = UnitT (Rd, NeverWr)
-  let uT = UnitT (NRd, NeverWr)
-
-  let rfT t = RefT (Rf, t)
-  let cpT t = RefT (Cp, t)
-
-  let moded t = ((In, NOut), t)
-
-  let defg t = VarD (t, UnitE)
-
-  (* - utils tests *)
-
-  let%expect_test "mem add / get / set" =
-    let mem = empty_mem in
-    let (mem, id1) = mem_add mem ZeroV in 
-    let (mem, id2) = mem_add mem SmthV in 
-    let (mem, id3) = mem_add mem BotV in 
-    Printf.printf "%i %i %i " id1 id2 id3;
-    Printf.printf "%b %b %b " (mem_get mem id1 == ZeroV)
-                              (mem_get mem id2 == SmthV)
-                              (mem_get mem id3 == BotV);
-    let mem = mem_set mem id1 BotV in 
-    let mem = mem_set mem id2 ZeroV in 
-    let mem = mem_set mem id3 SmthV in 
-    Printf.printf "%b %b %b" (mem_get mem id1 == BotV)
-                              (mem_get mem id2 == ZeroV)
-                              (mem_get mem id3 == SmthV);
-    [%expect {| 0 1 2 true true true true true true |}]
-
-  (* - basic var tests *)
+  (* - tests without functions *)
 
   let%expect_test "empty" =
     prog_eval_noret ([], SkipS);
@@ -449,49 +379,6 @@ struct
     with Eval_error msg -> Printf.printf "%s" msg;
     [%expect {| read |}]
 
-  let%expect_test "simple vars, no read & read" =
-    prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE);
-                      VarD (UnitT (Rd, MayWr), UnitE)],
-                     ReadS (VarP (globals_min_id + 1)));
-    Printf.printf "done!";
-    [%expect {| done! |}]
-
-  let%expect_test "simple var, write" =
-    prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE)], WriteS (VarP globals_min_id));
-    Printf.printf "done!";
-    [%expect {| done! |}]
-
-  let%expect_test "simple var, no write" =
-    try(prog_eval_noret ([VarD (UnitT (NRd, NeverWr), UnitE)], WriteS (VarP globals_min_id));
-         [%expect.unreachable]);
-    with Eval_error msg -> Printf.printf "%s" msg;
-    [%expect {| write: write tag |}]
-
-  let%expect_test "simple var, write & read" =
-    prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE)], SeqS (WriteS (VarP globals_min_id),
-                                                               ReadS (VarP globals_min_id)));
-    Printf.printf "done!";
-    [%expect {| done! |}]
-
-  (* - basic call tests *)
-
-  let%expect_test "simple call with read" =
-    prog_eval_noret ([VarD (UnitT (Rd, NeverWr), UnitE);
-                      FunD ([(In, NOut), UnitT (Rd, NeverWr)], ReadS (VarP 0))],
-                     CallS (VarP (globals_min_id + 1),
-                            [PathE (VarP globals_min_id)]));
-    Printf.printf "done!";
-    [%expect {| done! |}]
-
-  let%expect_test "simple call with write" =
-    prog_eval_noret ([VarD ((UnitT (Rd, MayWr)), UnitE);
-                      VarD (RefT (Rf, (UnitT (Rd, MayWr))), RefE globals_min_id);
-                      FunD ([(In, NOut), RefT (Cp, UnitT (Rd, MayWr))], WriteS (DerefP (VarP 0)))],
-                     CallS (VarP (globals_min_id + 2),
-                            [PathE (VarP (globals_min_id + 1))]));
-    Printf.printf "done!";
-    [%expect {| done! |}]
-
   (* --- FIXME --- CURRENT REWRITE POINT --- FIXME --- *)
 
   (* --- tests --- *)
diff --git a/model_with_structures/dune b/model_with_structures/dune
index 54383e4..489258f 100644
--- a/model_with_structures/dune
+++ b/model_with_structures/dune
@@ -42,23 +42,23 @@
 ;    -pp
 ;    camlp5/pp5+gt+plugins+ocanren+dump.exe)))
 
-(library
- (name synthesizer_st)
- (modules synthesizer)
- (flags
-  ; (-dsource)
-  (:standard -rectypes))
- (libraries OCanren OCanren.tester)
- (preprocessor_deps ../camlp5/pp5+gt+plugins+ocanren+dump.exe)
- (wrapped false)
- (preprocess
-  (pps
-   OCanren-ppx.ppx_repr
-   OCanren-ppx.ppx_deriving_reify
-   OCanren-ppx.ppx_fresh
-   GT.ppx
-   GT.ppx_all
-   OCanren-ppx.ppx_distrib
-   --
-   -pp
-   camlp5/pp5+gt+plugins+ocanren+dump.exe)))
+; (library
+;  (name synthesizer_st)
+;  (modules synthesizer)
+;  (flags
+;   ; (-dsource)
+;   (:standard -rectypes))
+;  (libraries OCanren OCanren.tester)
+;  (preprocessor_deps ../camlp5/pp5+gt+plugins+ocanren+dump.exe)
+;  (wrapped false)
+;  (preprocess
+;   (pps
+;    OCanren-ppx.ppx_repr
+;    OCanren-ppx.ppx_deriving_reify
+;    OCanren-ppx.ppx_fresh
+;    GT.ppx
+;    GT.ppx_all
+;    OCanren-ppx.ppx_distrib
+;    --
+;    -pp
+;    camlp5/pp5+gt+plugins+ocanren+dump.exe)))
diff --git a/model_with_structures/model.typ b/model_with_structures/model.typ
index 6b4cf41..3742b24 100644
--- a/model_with_structures/model.typ
+++ b/model_with_structures/model.typ
@@ -112,9 +112,8 @@
     {
       Or[$()$][value of simple type] // `Unit`
       Or[$path$][value from variable] // `Path`
-      // TODO FIXME: expand to support arbitrary paths (that do lead to lvalue)
-      // add relation to calc lvalue / rvalue for each element ?
-      Or[$rf X$][reference expr] // `Ref`
+      // TODO: decide what is the result of ref expr eval
+      // Or[$rf expr$][reference expr] // `Ref`
       Or[$[expr+]$][tuple expr] // `Prod`
     }
   ),
@@ -653,7 +652,7 @@ $s in stmt, f in X, x in X, a in X$
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ unit expr value],
+    name: [ unit value type],
 
     $vals, mu texpre () eqmu 0$,
   )
@@ -662,26 +661,32 @@ $s in stmt, f in X, x in X, a in X$
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ path expr value],
+    name: [ path type],
 
     $vals, mu tval p eqmu v$,
     $vals, mu texpre p eqmu v$,
   )
 ))
 
-#align(center, prooftree(
-  vertical-spacing: 4pt,
-  rule(
-    name: [ ref expr value],
+// NOTE: tmp removed
+// #align(center, prooftree(
+//   vertical-spacing: 4pt,
+//   rule(
+//     name: [ unit value type],
 
-    $vals, mu texpre rf x eqmu rf vals[x]$,
-  )
-))
+//     $vals, mu texpre e : t$,
+
+//     [*TODO*],
+
+//     // TODO: reference to what ??
+//     $vals, mu texpre rf e eqmu rf ??$,
+//   )
+// ))
 
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ tuple expr value],
+    name: [ unit value type],
 
     $vals, mu texpre e_1 eqmu v_1$,
     $...$,
@@ -699,7 +704,7 @@ $s in stmt, f in X, x in X, a in X$
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ unit value expr type],
+    name: [ unit value type],
 
     $types texprt () : cl Read, NotWrite cr$,
   )
@@ -708,26 +713,29 @@ $s in stmt, f in X, x in X, a in X$
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ path expr type],
+    name: [ path type],
 
     $types ttype p : t$,
     $types texprt p : t$,
   )
 ))
 
-#align(center, prooftree(
-  vertical-spacing: 4pt,
-  rule(
-    name: [ ref expr type],
+// NOTE: tmp removed
+// #align(center, prooftree(
+//   vertical-spacing: 4pt,
+//   rule(
+//     name: [ unit value type],
 
-    $types texprt rf x : rf Ref types[x]$,
-  )
-))
+//     $types texprt e : t$,
+//     // TODO: why Ref mode ?? <- due to immutability ??
+//     $types texprt rf e : rf Ref t$,
+//   )
+// ))
 
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ tuple expr type],
+    name: [ unit value type],
 
     $types texprt e_1 : t_1$,
     $...$,
@@ -920,21 +928,7 @@ $s in stmt, f in X, x in X, a in X$
   rule(
     name: [ full spoil for tuple expr],
 
-    // NOTE: x as path
-    $mu stretch(=>)^(m space t space x)_(cl vals, types cr) mu'$,
-
-    // TODO:: is c important ?
-    $mu stretch(=>)^(m space rf c t space rf x_(cl vals, types cr) mu'$,
-  )
-))
-
-#h(10pt)
-
-#align(center, prooftree(
-  vertical-spacing: 4pt,
-  rule(
-    name: [ full spoil for tuple expr],
-
+    $e = [e_1, ... e_n]$,
     $mu_0 stretch(=>)^(m space t_1 space e_1)_(cl vals, types cr) mu_1$,
     $...$,
     $mu_(n - 1) stretch(=>)^(m space t_n space e_n)_(cl vals, types cr) mu_n$,
diff --git a/model_with_structures/synthesizer.ml b/model_with_structures/synthesizer.ml
index 696722b..02d5250 100644
--- a/model_with_structures/synthesizer.ml
+++ b/model_with_structures/synthesizer.ml
@@ -1,7 +1,7 @@
 module Relational =
 struct
   open GT
-  (* open OCanren *)
+  open OCanren
   open OCanren.Std
 
   type data_ground = Nat.ground (* with show, gmap *)
@@ -28,10 +28,11 @@ struct
     ]
   end
 
+  (* NOTE: rename names ?? *)
   module CopyCap = struct
     [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
     [%%ocanren_inject
-      type nonrec t = Rf | Cp
+      type nonrec t = Ref | Val
       [@@deriving gt ~options:{ show; gmap }]
       type nonrec ground = t
     ]
@@ -56,495 +57,493 @@ struct
     ]
   end
 
-  (* --- FIXME --- CURRENT REWRITE POINT --- FIXME --- *)
-
-  (* module Tag = struct *)
-    (* [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] *)
-    (* [%%ocanren_inject *)
-      (* type nonrec ('r, 'w, 'c, 'i, 'o) t = Tag of 'r * 'w * 'c * 'i * 'o *)
-      (* [@@deriving gt ~options:{ show; gmap }] *)
-      (* type nonrec ground = (ReadCap.ground, WriteCap.ground, CopyCap.ground, InCap.ground, OutCap.ground) t *)
-    (* ] *)
+  module Tag = struct
+    [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
+    [%%ocanren_inject
+      type nonrec ('r, 'w, 'c, 'i, 'o) t = Tag of 'r * 'w * 'c * 'i * 'o
+      [@@deriving gt ~options:{ show; gmap }]
+      type nonrec ground = (ReadCap.ground, WriteCap.ground, CopyCap.ground, InCap.ground, OutCap.ground) t
+    ]
 
     (* TODO: less repeats *)
     (* common constructors *)
-    (* let rwi_val = let open ReadCap in *)
-                  (* let open WriteCap in *)
-                  (* let open CopyCap in *)
-                  (* let open InCap in *)
-                  (* let open OutCap in *)
-                  (* ocanren { Tag (Rd, AlwaysWr, Val, In, NOut) } *)
-    (* let ri_val = let open ReadCap in *)
-                 (* let open WriteCap in *)
-                 (* let open CopyCap in *)
-                 (* let open InCap in *)
-                 (* let open OutCap in *)
-                 (* ocanren { Tag (Rd, NeverWr, Val, In, NOut) } *)
-    (* let wi_val = let open ReadCap in *)
-                 (* let open WriteCap in *)
-                 (* let open CopyCap in *)
-                 (* let open InCap in *)
-                 (* let open OutCap in *)
-                 (* ocanren { Tag (NRd, AlwaysWr, Val, In, NOut) } *)
-    (* let i_val = let open ReadCap in *)
-                (* let open WriteCap in *)
-                (* let open CopyCap in *)
-                (* let open InCap in *)
-                (* let open OutCap in *)
-                (* ocanren { Tag (NRd, NeverWr, Val, In, NOut) } *)
-    (* let rwi_ref = let open ReadCap in *)
-                  (* let open WriteCap in *)
-                  (* let open CopyCap in *)
-                  (* let open InCap in *)
-                  (* let open OutCap in *)
-                  (* ocanren { Tag (Rd, AlwaysWr, Ref, In, NOut) } *)
-    (* let ri_ref = let open ReadCap in *)
-                 (* let open WriteCap in *)
-                 (* let open CopyCap in *)
-                 (* let open InCap in *)
-                 (* let open OutCap in *)
-                 (* ocanren { Tag (Rd, NeverWr, Ref, In, NOut) } *)
-    (* let wi_ref = let open ReadCap in *)
-                 (* let open WriteCap in *)
-                 (* let open CopyCap in *)
-                 (* let open InCap in *)
-                 (* let open OutCap in *)
-                 (* ocanren { Tag (NRd, AlwaysWr, Ref, In, NOut) } *)
-    (* let i_ref = let open ReadCap in *)
-                (* let open WriteCap in *)
-                (* let open CopyCap in *)
-                (* let open InCap in *)
-                (* let open OutCap in *)
-                (* ocanren { Tag (NRd, NeverWr, Ref, In, NOut) } *)
+    let rwi_val = let open ReadCap in
+                  let open WriteCap in
+                  let open CopyCap in
+                  let open InCap in
+                  let open OutCap in
+                  ocanren { Tag (Rd, AlwaysWr, Val, In, NOut) }
+    let ri_val = let open ReadCap in
+                 let open WriteCap in
+                 let open CopyCap in
+                 let open InCap in
+                 let open OutCap in
+                 ocanren { Tag (Rd, NeverWr, Val, In, NOut) }
+    let wi_val = let open ReadCap in
+                 let open WriteCap in
+                 let open CopyCap in
+                 let open InCap in
+                 let open OutCap in
+                 ocanren { Tag (NRd, AlwaysWr, Val, In, NOut) }
+    let i_val = let open ReadCap in
+                let open WriteCap in
+                let open CopyCap in
+                let open InCap in
+                let open OutCap in
+                ocanren { Tag (NRd, NeverWr, Val, In, NOut) }
+    let rwi_ref = let open ReadCap in
+                  let open WriteCap in
+                  let open CopyCap in
+                  let open InCap in
+                  let open OutCap in
+                  ocanren { Tag (Rd, AlwaysWr, Ref, In, NOut) }
+    let ri_ref = let open ReadCap in
+                 let open WriteCap in
+                 let open CopyCap in
+                 let open InCap in
+                 let open OutCap in
+                 ocanren { Tag (Rd, NeverWr, Ref, In, NOut) }
+    let wi_ref = let open ReadCap in
+                 let open WriteCap in
+                 let open CopyCap in
+                 let open InCap in
+                 let open OutCap in
+                 ocanren { Tag (NRd, AlwaysWr, Ref, In, NOut) }
+    let i_ref = let open ReadCap in
+                let open WriteCap in
+                let open CopyCap in
+                let open InCap in
+                let open OutCap in
+                ocanren { Tag (NRd, NeverWr, Ref, In, NOut) }
 
     (* constraints *)
-    (* let x_any tag = let open InCap in *)
-                    (* let open OutCap in *)
-                    (* ocanren { fresh r, w, c in *)
-                              (* tag == Tag (r, w, c, NIn, NOut) } *)
-    (* let i_any tag = let open InCap in *)
-                    (* let open OutCap in *)
-                    (* ocanren { fresh r, w, c in *)
-                              (* tag == Tag (r, w, c, In, NOut) } *)
-    (* let o_any tag = let open InCap in *)
-                    (* let open OutCap in *)
-                    (* ocanren { fresh r, w, c in *)
-                              (* tag == Tag (r, w, c, NIn, Out) } *)
-    (* let io_any tag = let open InCap in *)
-                     (* let open OutCap in *)
-                     (* ocanren { fresh r, w, c in *)
-                               (* tag == Tag (r, w, c, In, Out) } *)
+    let x_any tag = let open InCap in
+                    let open OutCap in
+                    ocanren { fresh r, w, c in
+                              tag == Tag (r, w, c, NIn, NOut) }
+    let i_any tag = let open InCap in
+                    let open OutCap in
+                    ocanren { fresh r, w, c in
+                              tag == Tag (r, w, c, In, NOut) }
+    let o_any tag = let open InCap in
+                    let open OutCap in
+                    ocanren { fresh r, w, c in
+                              tag == Tag (r, w, c, NIn, Out) }
+    let io_any tag = let open InCap in
+                     let open OutCap in
+                     ocanren { fresh r, w, c in
+                               tag == Tag (r, w, c, In, Out) }
 
     (* accessors *)
-    (* let is_reado tag = let open ReadCap in ocanren { *)
-                         (* fresh w_, c_, i_, o_ in *)
-                         (* tag == Tag (Rd, w_, c_, i_, o_) } *)
-    (* let is_not_reado tag = let open ReadCap in ocanren { *)
-                             (* fresh w_, c_, i_, o_ in *)
-                             (* tag == Tag (NRd, w_, c_, i_, o_) } *)
-    (* let is_always_writeo tag = let open WriteCap in ocanren { *)
-                                 (* fresh r_, c_, i_, o_ in *)
-                                 (* tag == Tag (r_, AlwaysWr, c_, i_, o_) } *)
-    (* let is_may_writeo tag = let open WriteCap in ocanren { *)
-                              (* fresh r_, c_, i_, o_ in *)
-                              (* { tag == Tag (r_, AlwaysWr, c_, i_, o_) | *)
-                                (* tag == Tag (r_, MayWr, c_, i_, o_) } } *)
-    (* let is_never_writeo tag = let open WriteCap in ocanren { *)
-                                (* fresh r_, c_, i_, o_ in *)
-                                (* tag == Tag (r_, NeverWr, c_, i_, o_) } *)
-    (* let is_refo tag = let open CopyCap in ocanren { *)
-                        (* fresh r_, w_, i_, o_ in *)
-                        (* tag == Tag (r_, w_, Ref, i_, o_) } *)
-    (* let is_valueo tag = let open CopyCap in ocanren { *)
-                          (* fresh r_, w_, i_, o_ in *)
-                          (* tag == Tag (r_, w_, Val, i_, o_) } *)
-    (* let is_ino tag = let open InCap in ocanren { *)
-                       (* fresh r_, w_, c_, o_ in *)
-                       (* tag == Tag (r_, w_, c_, In, o_) } *)
-    (* let is_not_ino tag = let open InCap in ocanren { *)
-                           (* fresh r_, w_, c_, o_ in *)
-                           (* tag == Tag (r_, w_, c_, NIn, o_) } *)
-    (* let is_outo tag = let open OutCap in ocanren { *)
-                        (* fresh r_, w_, c_, i_ in *)
-                        (* tag == Tag (r_, w_, c_, i_, Out) } *)
-    (* let is_not_outo tag = let open OutCap in ocanren { *)
-                            (* fresh r_, w_, c_, i_ in *)
-                            (* tag == Tag (r_, w_, c_, i_, NOut) } *)
+    let is_reado tag = let open ReadCap in ocanren {
+                         fresh w_, c_, i_, o_ in
+                         tag == Tag (Rd, w_, c_, i_, o_) }
+    let is_not_reado tag = let open ReadCap in ocanren {
+                             fresh w_, c_, i_, o_ in
+                             tag == Tag (NRd, w_, c_, i_, o_) }
+    let is_always_writeo tag = let open WriteCap in ocanren {
+                                 fresh r_, c_, i_, o_ in
+                                 tag == Tag (r_, AlwaysWr, c_, i_, o_) }
+    let is_may_writeo tag = let open WriteCap in ocanren {
+                              fresh r_, c_, i_, o_ in
+                              { tag == Tag (r_, AlwaysWr, c_, i_, o_) |
+                                tag == Tag (r_, MayWr, c_, i_, o_) } }
+    let is_never_writeo tag = let open WriteCap in ocanren {
+                                fresh r_, c_, i_, o_ in
+                                tag == Tag (r_, NeverWr, c_, i_, o_) }
+    let is_refo tag = let open CopyCap in ocanren {
+                        fresh r_, w_, i_, o_ in
+                        tag == Tag (r_, w_, Ref, i_, o_) }
+    let is_valueo tag = let open CopyCap in ocanren {
+                          fresh r_, w_, i_, o_ in
+                          tag == Tag (r_, w_, Val, i_, o_) }
+    let is_ino tag = let open InCap in ocanren {
+                       fresh r_, w_, c_, o_ in
+                       tag == Tag (r_, w_, c_, In, o_) }
+    let is_not_ino tag = let open InCap in ocanren {
+                           fresh r_, w_, c_, o_ in
+                           tag == Tag (r_, w_, c_, NIn, o_) }
+    let is_outo tag = let open OutCap in ocanren {
+                        fresh r_, w_, c_, i_ in
+                        tag == Tag (r_, w_, c_, i_, Out) }
+    let is_not_outo tag = let open OutCap in ocanren {
+                            fresh r_, w_, c_, i_ in
+                            tag == Tag (r_, w_, c_, i_, NOut) }
 
-    (* let eq_copyo tag cp = let open CopyCap in ocanren { *)
-                           (* fresh r_, w_, i_, o_ in *)
-                           (* tag == Tag (r_, w_, cp, i_, o_) } *)
+    let eq_copyo tag cp = let open CopyCap in ocanren {
+                           fresh r_, w_, i_, o_ in
+                           tag == Tag (r_, w_, cp, i_, o_) }
 
-    (* module Test = struct *)
-      (* @type answer = logic GT.list with show *)
+    module Test = struct
+      @type answer = logic GT.list with show
 
-      (* let test _ = show(answer) (Stream.take (run q (fun q -> let open ReadCap in *)
-                                                              (* let open WriteCap in *)
-                                                              (* let open CopyCap in *)
-                                                              (* let open InCap in *)
-                                                              (* let open OutCap in *)
-                                                              (* ocanren {q == Tag (Rd, NeverWr, Ref, In, NOut)}) *)
-                                                    (* (fun q -> q#reify reify))) *)
-    (* end *)
-  (* end *)
+      let test _ = show(answer) (Stream.take (run q (fun q -> let open ReadCap in
+                                                              let open WriteCap in
+                                                              let open CopyCap in
+                                                              let open InCap in
+                                                              let open OutCap in
+                                                              ocanren {q == Tag (Rd, NeverWr, Ref, In, NOut)})
+                                                    (fun q -> q#reify reify)))
+    end
+  end
 
-  (* module Stmt = struct *)
-    (* [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] *)
-    (* [%%ocanren_inject *)
-      (* type nonrec ('d, 'dl, 'sl) t = Call of 'd * 'dl | Read of 'd | Write of 'd | Choice of 'sl * 'sl *)
-      (* [@@deriving gt ~options:{ show; gmap }] *)
-      (* type ground = (Nat.ground, Nat.ground List.ground, ground List.ground) t *)
-    (* ] *)
+  module Stmt = struct
+    [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
+    [%%ocanren_inject
+      type nonrec ('d, 'dl, 'sl) t = Call of 'd * 'dl | Read of 'd | Write of 'd | Choice of 'sl * 'sl
+      [@@deriving gt ~options:{ show; gmap }]
+      type ground = (Nat.ground, Nat.ground List.ground, ground List.ground) t
+    ]
 
-    (* module Test = struct *)
-      (* @type answer = Nat.ground List.ground GT.list with show *)
-      (* @type answer'  = ground GT.list with show *)
+    module Test = struct
+      @type answer = Nat.ground List.ground GT.list with show
+      @type answer'  = ground GT.list with show
 
-      (* let test1 _ = show(answer) (Stream.take (run q (fun q -> ocanren {Call (1, [2]) == Call (1, q)}) *)
-                                                     (* (fun q -> q#reify (List.prj_exn Nat.prj_exn)))) *)
+      let test1 _ = show(answer) (Stream.take (run q (fun q -> ocanren {Call (1, [2]) == Call (1, q)})
+                                                     (fun q -> q#reify (List.prj_exn Nat.prj_exn))))
 
-      (* let test2 _ = show(answer') (Stream.take (run q (fun q -> ocanren {Call (1, [2]) == q}) *)
-                                                      (* (fun q -> q#reify (prj_exn)))) *)
-    (* end *)
-  (* end *)
+      let test2 _ = show(answer') (Stream.take (run q (fun q -> ocanren {Call (1, [2]) == q})
+                                                      (fun q -> q#reify (prj_exn))))
+    end
+  end
 
-  (* module FunDecl = struct *)
-    (* [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] *)
-    (* [%%ocanren_inject *)
-      (* type nonrec ('l, 'b) t = FunDecl of 'l * 'b *)
-      (* [@@deriving gt ~options:{ show; gmap }] *)
-      (* type nonrec ground = (Tag.ground List.ground, Stmt.ground List.ground) t *)
-    (* ] *)
+  module FunDecl = struct
+    [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
+    [%%ocanren_inject
+      type nonrec ('l, 'b) t = FunDecl of 'l * 'b
+      [@@deriving gt ~options:{ show; gmap }]
+      type nonrec ground = (Tag.ground List.ground, Stmt.ground List.ground) t
+    ]
 
-    (* module Test = struct *)
-      (* @type answer  = ground GT.list with show *)
-      (* let test _ = show(answer) (Stream.take (run q (fun q -> let open Tag in *)
-                                                              (* let open Stmt in *)
-                                                              (* ocanren {FunDecl ([rwi_ref; rwi_val], [Call (1, [0]); Write 1]) == q}) *)
-                                                    (* (fun q -> q#reify (prj_exn)))) *)
-    (* end *)
-  (* end *)
+    module Test = struct
+      @type answer  = ground GT.list with show
+      let test _ = show(answer) (Stream.take (run q (fun q -> let open Tag in
+                                                              let open Stmt in
+                                                              ocanren {FunDecl ([rwi_ref; rwi_val], [Call (1, [0]); Write 1]) == q})
+                                                    (fun q -> q#reify (prj_exn))))
+    end
+  end
 
-  (* module Prog = struct *)
-    (* [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] *)
-    (* [%%ocanren_inject *)
-      (* type nonrec ('l, 'f) t = Prog of 'l * 'f *)
-      (* [@@deriving gt ~options:{ show; gmap }] *)
-      (* type nonrec ground = (FunDecl.ground List.ground, FunDecl.ground) t *)
-    (* ] *)
+  module Prog = struct
+    [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
+    [%%ocanren_inject
+      type nonrec ('l, 'f) t = Prog of 'l * 'f
+      [@@deriving gt ~options:{ show; gmap }]
+      type nonrec ground = (FunDecl.ground List.ground, FunDecl.ground) t
+    ]
 
-    (* module Test = struct *)
-      (* @type answer  = ground GT.list with show *)
-      (* let test _ = show(answer) (Stream.take (run q (fun q -> let open FunDecl in *)
-                                                              (* let open Tag in *)
-                                                              (* let open Stmt in *)
-                                                              (* ocanren {Prog ([], FunDecl ([ri_val], [Write 0; Read 0])) == q}) *)
-                                                    (* (fun q -> q#reify (prj_exn)))) *)
-    (* end *)
-  (* end *)
+    module Test = struct
+      @type answer  = ground GT.list with show
+      let test _ = show(answer) (Stream.take (run q (fun q -> let open FunDecl in
+                                                              let open Tag in
+                                                              let open Stmt in
+                                                              ocanren {Prog ([], FunDecl ([ri_val], [Write 0; Read 0])) == q})
+                                                    (fun q -> q#reify (prj_exn))))
+    end
+  end
 
-  (* module Arg = struct *)
-    (* [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] *)
-    (* [%%ocanren_inject *)
-      (* type nonrec 'd t = RValue | LValue of 'd *)
-      (* [@@deriving gt ~options:{ show; gmap }] *)
-      (* type nonrec ground = Nat.ground t *)
-    (* ] *)
+  module Arg = struct
+    [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
+    [%%ocanren_inject
+      type nonrec 'd t = RValue | LValue of 'd
+      [@@deriving gt ~options:{ show; gmap }]
+      type nonrec ground = Nat.ground t
+    ]
 
-    (* module Test = struct *)
-      (* @type answer = logic GT.list with show *)
-      (* let test _ = show(answer) (Stream.take (run q (fun q -> ocanren {q == LValue 3}) *)
-                                                    (* (fun q -> q#reify reify))) *)
-    (* end *)
-  (* end *)
+    module Test = struct
+      @type answer = logic GT.list with show
+      let test _ = show(answer) (Stream.take (run q (fun q -> ocanren {q == LValue 3})
+                                                    (fun q -> q#reify reify)))
+    end
+  end
 
-  (* module Value = struct *)
-    (* [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] *)
-    (* [%%ocanren_inject *)
-      (* type nonrec t = Unit | Undef | Bot *)
-      (* [@@deriving gt ~options:{ show; gmap }] *)
-      (* type nonrec ground = t *)
-    (* ] *)
+  module Value = struct
+    [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
+    [%%ocanren_inject
+      type nonrec t = Unit | Undef | Bot
+      [@@deriving gt ~options:{ show; gmap }]
+      type nonrec ground = t
+    ]
 
-    (* module Test = struct *)
-      (* @type answer = logic GT.list with show *)
-      (* let test _ = show(answer) (Stream.take (run q (fun q -> ocanren {q == Bot | q == Unit}) *)
-                                                    (* (fun q -> q#reify reify))) *)
-    (* end *)
-  (* end *)
+    module Test = struct
+      @type answer = logic GT.list with show
+      let test _ = show(answer) (Stream.take (run q (fun q -> ocanren {q == Bot | q == Unit})
+                                                    (fun q -> q#reify reify)))
+    end
+  end
 
-  (* module St = struct *)
-    (* [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] *)
-    (* [%%ocanren_inject *)
-      (* type nonrec ('env, 'mem, 'last_mem, 'visited) t = St of 'env * 'mem * 'last_mem * 'visited *)
-      (* [@@deriving gt ~options:{ show; gmap }] *)
-      (* type nonrec ground = (((Nat.ground, ((Tag.ground, Nat.ground) Pair.ground)) Pair.ground) List.ground, *)
-                            (* Value.ground List.ground, Nat.ground, Nat.ground List.ground) t *)
-    (* ] *)
+  module St = struct
+    [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
+    [%%ocanren_inject
+      type nonrec ('env, 'mem, 'last_mem, 'visited) t = St of 'env * 'mem * 'last_mem * 'visited
+      [@@deriving gt ~options:{ show; gmap }]
+      type nonrec ground = (((Nat.ground, ((Tag.ground, Nat.ground) Pair.ground)) Pair.ground) List.ground,
+                            Value.ground List.ground, Nat.ground, Nat.ground List.ground) t
+    ]
 
-    (* module Test = struct *)
-      (* @type answer  = ground GT.list with show *)
-      (* let test _ = show(answer) (Stream.take (run q (fun q -> let open Value in *)
-                                                              (* let open Tag in *)
-                                                              (* ocanren {St ([Std.pair 0 (Std.pair rwi_val 0)], [Bot], 1, [0]) == q}) *)
-                                                    (* (fun q -> q#reify (prj_exn)))) *)
-    (* end *)
-  (* end *)
+    module Test = struct
+      @type answer  = ground GT.list with show
+      let test _ = show(answer) (Stream.take (run q (fun q -> let open Value in
+                                                              let open Tag in
+                                                              ocanren {St ([Std.pair 0 (Std.pair rwi_val 0)], [Bot], 1, [0]) == q})
+                                                    (fun q -> q#reify (prj_exn))))
+    end
+  end
 
   (* --- *)
 
-  (* let rec list_zip_witho f xs ys zs = ocanren { *)
-    (* { fresh x, xs', y, ys', z, zs' in *)
-      (* xs == x :: xs' & *)
-      (* ys == y :: ys' & *)
-      (* zs == z :: zs' & *)
-      (* f x y z & *)
-      (* list_zip_witho f xs' ys' zs' } | *)
-    (* { fresh x, xs' in *)
-      (* xs == x :: xs' & *)
-      (* ys == [] & *)
-      (* zs == [] } | *)
-    (* { fresh y, ys' in *)
-      (* xs == [] & *)
-      (* ys == y :: ys' & *)
-      (* zs == [] } | *)
-    (* { xs == [] & ys == [] & zs == [] } *)
-  (* } *)
+  let rec list_zip_witho f xs ys zs = ocanren {
+    { fresh x, xs', y, ys', z, zs' in
+      xs == x :: xs' &
+      ys == y :: ys' &
+      zs == z :: zs' &
+      f x y z &
+      list_zip_witho f xs' ys' zs' } |
+    { fresh x, xs' in
+      xs == x :: xs' &
+      ys == [] &
+      zs == [] } |
+    { fresh y, ys' in
+      xs == [] &
+      ys == y :: ys' &
+      zs == [] } |
+    { xs == [] & ys == [] & zs == [] }
+  }
 
   (* --- *)
 
-  (* let value_combineo left right res = let open Value in ocanren { *)
-    (* { left == Unit & right == Unit & res == Unit } | *)
-    (* { left == Bot & right == Bot & res == Bot } | *)
-    (* { left == Unit & right == Bot & res == Undef } | *)
-    (* { left == Bot & right == Unit & res == Undef } *)
-  (* } *)
+  let value_combineo left right res = let open Value in ocanren {
+    { left == Unit & right == Unit & res == Unit } |
+    { left == Bot & right == Bot & res == Bot } |
+    { left == Unit & right == Bot & res == Undef } |
+    { left == Bot & right == Unit & res == Undef }
+  }
 
-  (* let memory_combineo left right res = ocanren { *)
-    (* list_zip_witho value_combineo left right res *)
-  (* } *)
+  let memory_combineo left right res = ocanren {
+    list_zip_witho value_combineo left right res
+  }
 
-  (* let state_combineo left right res = let open St in ocanren { *)
-    (* fresh lenv, lmem, lmem_len, lvisited, renv, rmem, rmem_len, rvisited, res_mem in *)
-    (* left == St (lenv, lmem, lmem_len, lvisited) & *)
-    (* right == St (renv, rmem, rmem_len, rvisited) & *)
-    (* lenv == renv & lmem_len == rmem_len & *)
-    (* memory_combineo lmem rmem res_mem  & *)
-    (* res == St (lenv, rmem, lmem_len, List.appendo lvisited rvisited) *)
+  let state_combineo left right res = let open St in ocanren {
+    fresh lenv, lmem, lmem_len, lvisited, renv, rmem, rmem_len, rvisited, res_mem in
+    left == St (lenv, lmem, lmem_len, lvisited) &
+    right == St (renv, rmem, rmem_len, rvisited) &
+    lenv == renv & lmem_len == rmem_len &
+    memory_combineo lmem rmem res_mem  &
+    res == St (lenv, rmem, lmem_len, List.appendo lvisited rvisited)
     (* TODO: union visited lists instead ? *)
-  (* } *)
+  }
 
   (* --- *)
 
-  (* let rec list_replaceo xs id value ys = ocanren { *)
+  let rec list_replaceo xs id value ys = ocanren {
     (* xs == [] & ys == [] | (* NOTE: error *) *)
-    (* { fresh x, xs' in *)
-        (* xs == x :: xs' & *)
-        (* id == Nat.o & *)
-        (* ys == value :: xs' } | *)
-    (* { fresh x, xs', id', ys' in *)
-        (* xs == x :: xs' & *)
-        (* id == Nat.s id' & *)
-        (* ys == x :: ys' & *)
-        (* list_replaceo xs' id' value ys' } *)
-  (* } *)
+    { fresh x, xs' in
+        xs == x :: xs' &
+        id == Nat.o &
+        ys == value :: xs' } |
+    { fresh x, xs', id', ys' in
+        xs == x :: xs' &
+        id == Nat.s id' &
+        ys == x :: ys' &
+        list_replaceo xs' id' value ys' }
+  }
 
-  (* let env_geto state id tag' mem_id' = *)
-    (* let open St in *)
-    (* ocanren { *)
-    (* fresh env, _mem, _mem_len, _visited, elem in *)
-      (* state == St (env, _mem, _mem_len, _visited) & *)
-      (* List.assoco id env elem & *)
-      (* Std.pair tag' mem_id' == elem *)
-  (* } *)
+  let env_geto state id tag' mem_id' =
+    let open St in
+    ocanren {
+    fresh env, _mem, _mem_len, _visited, elem in
+      state == St (env, _mem, _mem_len, _visited) &
+      List.assoco id env elem &
+      Std.pair tag' mem_id' == elem
+  }
 
-  (* let env_addo state id tg mem_id state' = *)
-    (* let open St in *)
-    (* ocanren { *)
-    (* fresh env, env', mem, mem_len, visited, elem in *)
-      (* state == St (env, mem, mem_len, visited) & *)
-      (* Std.pair tg mem_id == elem & *) 
-      (* (Std.pair id elem) :: env == env' & *)
-      (* state' == St (env', mem, mem_len, visited) *)
-  (* } *)
+  let env_addo state id tg mem_id state' =
+    let open St in
+    ocanren {
+    fresh env, env', mem, mem_len, visited, elem in
+      state == St (env, mem, mem_len, visited) &
+      Std.pair tg mem_id == elem & 
+      (Std.pair id elem) :: env == env' &
+      state' == St (env', mem, mem_len, visited)
+  }
 
-  (* let inv_ido mem_len id id' = ocanren { *)
-    (* fresh inv_id_inc in *)
-      (* Nat.addo inv_id_inc id mem_len & *)
-      (* Nat.addo id' 1 inv_id_inc *)
-  (* } *)
+  let inv_ido mem_len id id' = ocanren {
+    fresh inv_id_inc in
+      Nat.addo inv_id_inc id mem_len &
+      Nat.addo id' 1 inv_id_inc
+  }
 
   (* --- *)
 
-  (* let rec list_ntho xs id x' = ocanren { *)
+  let rec list_ntho xs id x' = ocanren {
     (* xs == [] | (* NOTE: error *) *)
-    (* { fresh y', xs' in *)
-      (* id == Nat.o & *)
-      (* y' :: xs' == xs & *)
-      (* x' == y' } | *)
-    (* { fresh id', y', xs' in *)
-      (* Nat.s id' == id & *)
-      (* y' :: xs' == xs & *)
-      (* list_ntho xs' id' x' } *)
-  (* } *)
+    { fresh y', xs' in
+      id == Nat.o &
+      y' :: xs' == xs &
+      x' == y' } |
+    { fresh id', y', xs' in
+      Nat.s id' == id &
+      y' :: xs' == xs &
+      list_ntho xs' id' x' }
+  }
 
-  (* let mem_geto state id value' = *)
-    (* let open St in *)
-    (* ocanren { *)
-    (* fresh mem, mem_len, mem_id, mem_id_inv, _env, _visited, _tag in *)
-    (* state == St (_env, mem, mem_len, _visited) & *)
-    (* env_geto state id _tag mem_id & *)
-    (* inv_ido mem_len mem_id mem_id_inv & *)
-    (* list_ntho mem mem_id_inv value' *)
-  (* } *)
+  let mem_geto state id value' =
+    let open St in
+    ocanren {
+    fresh mem, mem_len, mem_id, mem_id_inv, _env, _visited, _tag in
+    state == St (_env, mem, mem_len, _visited) &
+    env_geto state id _tag mem_id &
+    inv_ido mem_len mem_id mem_id_inv &
+    list_ntho mem mem_id_inv value'
+  }
 
-  (* let mem_seto state id value state'= *)
-    (* let open St in *)
-    (* ocanren { *)
-    (* fresh env, mem, mem_len, visited, mem_id, inv_mem_id, mem', _tag in *)
-      (* state == St (env, mem, mem_len, visited) & *)
-      (* env_geto state id _tag mem_id & *)
-      (* inv_ido mem_len mem_id inv_mem_id & *)
-      (* list_replaceo mem inv_mem_id value mem' & *)
-      (* state' == St (env, mem', mem_len, visited) *)
-  (* } *)
+  let mem_seto state id value state'=
+    let open St in
+    ocanren {
+    fresh env, mem, mem_len, visited, mem_id, inv_mem_id, mem', _tag in
+      state == St (env, mem, mem_len, visited) &
+      env_geto state id _tag mem_id &
+      inv_ido mem_len mem_id inv_mem_id &
+      list_replaceo mem inv_mem_id value mem' &
+      state' == St (env, mem', mem_len, visited)
+  }
 
-  (* let mem_addo state value state' = *)
-    (* let open St in *)
-    (* ocanren { *)
-      (* fresh env, mem, mem_len, mem_len', visited, mem' in *)
-      (* state == St (env, mem, mem_len, visited) & *)
-      (* mem' == value :: mem & *)
-      (* mem_len' == Nat.s mem_len & *)
-      (* state' == St (env, mem', mem_len', visited) *)
-  (* } *)
+  let mem_addo state value state' =
+    let open St in
+    ocanren {
+      fresh env, mem, mem_len, mem_len', visited, mem' in
+      state == St (env, mem, mem_len, visited) &
+      mem' == value :: mem &
+      mem_len' == Nat.s mem_len &
+      state' == St (env, mem', mem_len', visited)
+  }
 
-  (* let mem_checko state id = *)
-    (* let open Value in *)
-    (* ocanren { *)
-      (* mem_geto state id Unit *)
-    (* } *)
+  let mem_checko state id =
+    let open Value in
+    ocanren {
+      mem_geto state id Unit
+    }
 
   (* --- *)
 
-  (* let rec list_foldlo f acc xs acc' = ocanren { *)
-    (* xs == [] & acc' == acc | *)
-    (* { fresh x', xs', acc_upd in *)
-      (* xs == x' :: xs' & *)
-      (* list_foldlo f acc xs' acc_upd & *)
-      (* f acc_upd x' acc' } *)
-  (* } *)
+  let rec list_foldlo f acc xs acc' = ocanren {
+    xs == [] & acc' == acc |
+    { fresh x', xs', acc_upd in
+      xs == x' :: xs' &
+      list_foldlo f acc xs' acc_upd &
+      f acc_upd x' acc' }
+  }
 
-  (* let rec list_foldro f acc xs acc' = ocanren { *)
-    (* xs == [] & acc' == acc | *)
-    (* { fresh x', xs', acc_upd in *)
-      (* xs == x' :: xs' & *)
-      (* f acc x' acc_upd & *)
-      (* list_foldro f acc_upd xs' acc' } *)
+  let rec list_foldro f acc xs acc' = ocanren {
+    xs == [] & acc' == acc |
+    { fresh x', xs', acc_upd in
+      xs == x' :: xs' &
+      f acc x' acc_upd &
+      list_foldro f acc_upd xs' acc' }
     (* TODO: inf search on swap, investigate *)
-  (* } *)
+  }
 
 
-  (* let rec list_foldr2o f acc xs ys acc' = ocanren { *)
-    (* xs == [] & ys == [] & acc' == acc | *)
-    (* { fresh x', xs', y', ys', acc_upd in *)
-      (* xs == x' :: xs' & *)
-      (* ys == y' :: ys' & *)
-      (* f acc x' y' acc_upd & *)
-      (* list_foldr2o f acc_upd xs' ys' acc' } *)
-  (* } *)
+  let rec list_foldr2o f acc xs ys acc' = ocanren {
+    xs == [] & ys == [] & acc' == acc |
+    { fresh x', xs', y', ys', acc_upd in
+      xs == x' :: xs' &
+      ys == y' :: ys' &
+      f acc x' y' acc_upd &
+      list_foldr2o f acc_upd xs' ys' acc' }
+  }
 
-  (* let rec list_foldl2o f acc xs ys acc' = ocanren { *)
-    (* xs == [] & ys == [] & acc' == acc | *)
-    (* { fresh x', xs', y', ys', acc_upd in *)
-      (* xs == x' :: xs' & *)
-      (* ys == y' :: ys' & *)
-      (* list_foldl2o f acc xs' ys' acc_upd & *)
-      (* f acc_upd x' y' acc' } *)
-  (* } *)
+  let rec list_foldl2o f acc xs ys acc' = ocanren {
+    xs == [] & ys == [] & acc' == acc |
+    { fresh x', xs', y', ys', acc_upd in
+      xs == x' :: xs' &
+      ys == y' :: ys' &
+      list_foldl2o f acc xs' ys' acc_upd &
+      f acc_upd x' y' acc' }
+  }
 
-  (* let arg_to_valueo state arg value' = *)
-    (* let open Arg in *)
-    (* let open Value in *)
-    (* ocanren { *)
-    (* arg == RValue & value' == Unit | *)
-    (* { fresh id in *)
-      (* arg == LValue id & *)
-      (* mem_geto state id value' } *)
-  (* } *)
+  let arg_to_valueo state arg value' =
+    let open Arg in
+    let open Value in
+    ocanren {
+    arg == RValue & value' == Unit |
+    { fresh id in
+      arg == LValue id &
+      mem_geto state id value' }
+  }
 
-  (* let arg_to_rvalueo arg value' = *)
-    (* let open Arg in *)
-    (* let open Tag in *)
-    (* ocanren { is_valueo arg & value' == RValue } *)
+  let arg_to_rvalueo arg value' =
+    let open Arg in
+    let open Tag in
+    ocanren { is_valueo arg & value' == RValue }
 
-  (* let st_mem_leno state mem_len' = *)
-    (* let open St in *)
-    (* ocanren { *)
-    (* fresh _env, _mem, _visited in *)
-      (* state == St (_env, _mem, mem_len', _visited) *)
-  (* } *)
+  let st_mem_leno state mem_len' =
+    let open St in
+    ocanren {
+    fresh _env, _mem, _visited in
+      state == St (_env, _mem, mem_len', _visited)
+  }
 
-  (* let tag_correcto tg = *)
-    (* let open Tag in *)
-    (* ocanren { *)
-      (* {is_not_outo tg | { is_outo tg & is_always_writeo tg } } & *)
-      (* {is_not_reado tg | { is_reado tg & is_ino tg } } *)
-    (* } *)
+  let tag_correcto tg =
+    let open Tag in
+    ocanren {
+      {is_not_outo tg | { is_outo tg & is_always_writeo tg } } &
+      {is_not_reado tg | { is_reado tg & is_ino tg } }
+    }
 
-  (* let st_add_argo state state_before id arg_tag arg state'' = *)
+  let st_add_argo state state_before id arg_tag arg state'' =
     (* let open Nat in *)
-    (* let open Value in *)
-    (* let open Arg in *)
-    (* let open Tag in *)
-    (* ocanren { *)
-        (* tag_correcto arg_tag & { *)
-        (* { fresh value', state', mem_len_prev' in *)
-          (* is_valueo arg_tag & *)
-          (* arg_to_valueo state_before arg value' & *)
-          (* mem_addo state value' state' & *)
-          (* st_mem_leno state mem_len_prev' & *)
-          (* env_addo state' id arg_tag mem_len_prev' state'' } | *)
-        (* { fresh arg', parent_tag, mem_id, state' in *)
-          (* is_refo arg_tag & *)
+    let open Value in
+    let open Arg in
+    let open Tag in
+    ocanren {
+        tag_correcto arg_tag & {
+        { fresh value', state', mem_len_prev' in
+          is_valueo arg_tag &
+          arg_to_valueo state_before arg value' &
+          mem_addo state value' state' &
+          st_mem_leno state mem_len_prev' &
+          env_addo state' id arg_tag mem_len_prev' state'' } |
+        { fresh arg', parent_tag, mem_id, state' in
+          is_refo arg_tag &
             (* { arg == RValue } *) (* NOTE: not allowed for now *)
-          (* arg == LValue arg' & *)
-          (* env_geto state_before id parent_tag mem_id & *)
-          (* env_addo state id arg_tag mem_id state' & *)
-          (* { is_never_writeo arg_tag | { is_may_writeo arg_tag & is_may_writeo parent_tag } } & *)
-          (* { *)
-            (* { is_reado arg_tag & state' == state'' } | *)
-            (* { is_not_reado arg_tag & mem_seto state' id Bot state'' } *)
-          (* } *)
-        (* } *)
-      (* } *)
-    (* } *)
+          arg == LValue arg' &
+          env_geto state_before id parent_tag mem_id &
+          env_addo state id arg_tag mem_id state' &
+          { is_never_writeo arg_tag | { is_may_writeo arg_tag & is_may_writeo parent_tag } } &
+          {
+            { is_reado arg_tag & state' == state'' } |
+            { is_not_reado arg_tag & mem_seto state' id Bot state'' }
+          }
+        }
+      }
+    }
 
-  (* let st_spoil_foldero state_before state tg id state' = *)
-    (* let open Value in *)
-    (* let open Tag in *)
-    (* let open St in *)
-    (* ocanren { *)
-      (* fresh env, mem, mem_len, _visited, parent_tg, _mem_id in *)
-      (* state == St (env, mem, mem_len, _visited) & *)
-      (* env_geto state id parent_tg _mem_id & *)
-      (* { is_not_reado tg | { is_reado tg & mem_checko state_before id } } & *)
-      (* { { is_never_writeo tg & state == state'} | *)
-        (* { is_always_writeo tg & *) 
-          (* is_outo tg & is_may_writeo parent_tg & mem_seto state id Unit state' } | *)
-        (* { is_may_writeo tg & { *)
-          (* { is_not_outo tg & is_valueo tg & state == state' } | *)
-          (* { is_not_outo tg & is_refo tg & is_may_writeo parent_tg & mem_seto state id Bot state' } *)
-        (* } } *)
-      (* } *)
-    (* } *)
+  let st_spoil_foldero state_before state tg id state' =
+    let open Value in
+    let open Tag in
+    let open St in
+    ocanren {
+      fresh env, mem, mem_len, _visited, parent_tg, _mem_id in
+      state == St (env, mem, mem_len, _visited) &
+      env_geto state id parent_tg _mem_id &
+      { is_not_reado tg | { is_reado tg & mem_checko state_before id } } &
+      { { is_never_writeo tg & state == state'} |
+        { is_always_writeo tg & 
+          is_outo tg & is_may_writeo parent_tg & mem_seto state id Unit state' } |
+        { is_may_writeo tg & {
+          { is_not_outo tg & is_valueo tg & state == state' } |
+          { is_not_outo tg & is_refo tg & is_may_writeo parent_tg & mem_seto state id Bot state' }
+        } }
+      }
+    }
 
-  (* let st_spoil_by_argso state arg_tags args state' = *)
-    (* ocanren { *)
-      (* fresh state_before in *)
-      (* state == state_before & (* TODO: required ? *) *)
-      (* list_foldl2o (st_spoil_foldero state_before) state arg_tags args state' *)
-    (* } *)
+  let st_spoil_by_argso state arg_tags args state' =
+    ocanren {
+      fresh state_before in
+      state == state_before & (* TODO: required ? *)
+      list_foldl2o (st_spoil_foldero state_before) state arg_tags args state'
+    }
 
   (* let st_spoil_assignmentso state state' = *)
     (* let open St in *)
@@ -556,150 +555,150 @@ struct
 
   (* --- *)
 
-  (* let arg_to_lvalueo arg arg' = *)
-    (* let open Arg in *)
-    (* ocanren { arg' == LValue arg } *)
+  let arg_to_lvalueo arg arg' =
+    let open Arg in
+    ocanren { arg' == LValue arg }
 
-  (* let rec list_dropo n xs xs' = ocanren { *)
-    (* xs == [] & xs' == [] | *)
-    (* n == Nat.o & xs == xs' & xs =/= [] | *)
-    (* { fresh n', _y, ys in *)
-        (* Nat.s n' == n & *)
-        (* xs == _y :: ys & *)
-        (* list_dropo n' ys xs' } *)
-  (* } *)
+  let rec list_dropo n xs xs' = ocanren {
+    xs == [] & xs' == [] |
+    n == Nat.o & xs == xs' & xs =/= [] |
+    { fresh n', _y, ys in
+        Nat.s n' == n &
+        xs == _y :: ys &
+        list_dropo n' ys xs' }
+  }
 
-  (* let rec list_not_membero xs x = ocanren { *)
-    (* xs == [] | *)
-    (* { fresh x', xs' in *)
-        (* xs == x' :: xs' & *)
-        (* x' =/= x & *)
-        (* list_not_membero xs' x } *)
-  (* } *)
+  let rec list_not_membero xs x = ocanren {
+    xs == [] |
+    { fresh x', xs' in
+        xs == x' :: xs' &
+        x' =/= x &
+        list_not_membero xs' x }
+  }
 
-  (* let visited_checko state f_id = *)
-    (* let open St in *)
-    (* ocanren { *)
-      (* fresh _env, _mem, _mem_len, visited in *)
-      (* state == St (_env, _mem, _mem_len, visited) & *)
-      (* List.membero visited f_id *)
-    (* } *)
+  let visited_checko state f_id =
+    let open St in
+    ocanren {
+      fresh _env, _mem, _mem_len, visited in
+      state == St (_env, _mem, _mem_len, visited) &
+      List.membero visited f_id
+    }
 
-  (* let not_visited_checko state f_id = *)
-    (* let open St in *)
-    (* ocanren { *)
-      (* fresh _env, _mem, _mem_len, visited in *)
-      (* state == St (_env, _mem, _mem_len, visited) & *)
-      (* list_not_membero visited f_id *)
-    (* } *)
+  let not_visited_checko state f_id =
+    let open St in
+    ocanren {
+      fresh _env, _mem, _mem_len, visited in
+      state == St (_env, _mem, _mem_len, visited) &
+      list_not_membero visited f_id
+    }
 
-  (* let visited_addo state f_id state' = *)
-    (* let open St in *)
-    (* ocanren { *)
-      (* fresh env, mem, mem_len, visited, visited' in *)
-      (* state == St (env, mem, mem_len, visited) & *)
-      (* visited' == f_id :: visited & *)
-      (* state' == St (env,mem, mem_len, visited') *)
-    (* } *)
+  let visited_addo state f_id state' =
+    let open St in
+    ocanren {
+      fresh env, mem, mem_len, visited, visited' in
+      state == St (env, mem, mem_len, visited) &
+      visited' == f_id :: visited &
+      state' == St (env,mem, mem_len, visited')
+    }
 
-  (* let rec eval_stmto state prog stmt state' = *)
-    (* let open Stmt in *)
-    (* let open Value in *)
-    (* let open FunDecl in *)
-    (* let open Tag in *)
-    (* ocanren { *)
-    (* { fresh f_id, args, f, args', state_after_call, arg_tags, _body in *)
-      (* stmt == Call (f_id, args) & *)
-      (* list_ntho prog f_id f & *)
-      (* FunDecl (arg_tags, _body) == f & *)
-      (* List.mapo arg_to_lvalueo args args' & *)
+  let rec eval_stmto state prog stmt state' =
+    let open Stmt in
+    let open Value in
+    let open FunDecl in
+    let open Tag in
+    ocanren {
+    { fresh f_id, args, f, args', state_after_call, arg_tags, _body in
+      stmt == Call (f_id, args) &
+      list_ntho prog f_id f &
+      FunDecl (arg_tags, _body) == f &
+      List.mapo arg_to_lvalueo args args' &
       (* TODO: FIXME: memoisation, do not do calls on check successfull *)
       
       (* NOTE: tmp simplification for less branching (TODO?) *)
-      (* { { fresh state_with_visited in *)
-          (* not_visited_checko state f_id & *)
-          (* visited_addo state f_id state_with_visited & *)
-          (* eval_funo state_with_visited prog f args' state_after_call } | *)
-        (* { visited_checko state f_id & *)
-          (* state_after_call == state } } & *)
-      (* st_spoil_by_argso state_after_call arg_tags args state' } | *)
-    (* { fresh id in stmt == Read id & mem_checko state id & state == state' } | *)
-    (* { fresh id, tag, _mem_id in *)
-      (* stmt == Write id & *)
-      (* env_geto state id tag _mem_id & *)
-      (* is_may_writeo tag & *)
-      (* mem_seto state id Unit state' } | *)
-    (* { fresh xs, ys in *)
-      (* stmt == Choice (xs, ys) } *)
+      { { fresh state_with_visited in
+          not_visited_checko state f_id &
+          visited_addo state f_id state_with_visited &
+          eval_funo state_with_visited prog f args' state_after_call } |
+        { visited_checko state f_id &
+          state_after_call == state } } &
+      st_spoil_by_argso state_after_call arg_tags args state' } |
+    { fresh id in stmt == Read id & mem_checko state id & state == state' } |
+    { fresh id, tag, _mem_id in
+      stmt == Write id &
+      env_geto state id tag _mem_id &
+      is_may_writeo tag &
+      mem_seto state id Unit state' } |
+    { fresh xs, ys in
+      stmt == Choice (xs, ys) }
     (* TODO: FIXME: choice actions *)
-  (* } *)
+  }
 
-  (* and eval_body_foldero prog state stmt state' = *)
-    (* eval_stmto state prog stmt state' *)
+  and eval_body_foldero prog state stmt state' =
+    eval_stmto state prog stmt state'
 
-  (* and eval_bodyo state prog body state' = *)
-    (* list_foldro (eval_body_foldero prog) state body state' *) 
+  and eval_bodyo state prog body state' =
+    list_foldro (eval_body_foldero prog) state body state' 
 
-  (* and add_arg_foldero state_before state_c arg_tag arg state_c' = *)
-    (* ocanren { *)
-    (* fresh state, id, state', id' in *)
-      (* state_c == Std.pair state id & *)
-      (* st_add_argo state state_before id arg_tag arg state' & *)
-      (* id' == Nat.s id & *)
-      (* state_c' == Std.pair state' id' *)
-  (* } *)
+  and add_arg_foldero state_before state_c arg_tag arg state_c' =
+    ocanren {
+    fresh state, id, state', id' in
+      state_c == Std.pair state id &
+      st_add_argo state state_before id arg_tag arg state' &
+      id' == Nat.s id &
+      state_c' == Std.pair state' id'
+  }
 
-  (* and eval_funo state prog decl args state' = *)
-    (* let open FunDecl in *)
-    (* let open St in *)
-    (* ocanren { *)
-    (* fresh arg_tags, body, *)
-          (* env_before, mem_before, len_before, visited_before, *)
-          (* state_clean, *)
-          (* state_with_vars, _counter, *)
-          (* state_evaled, *)
-          (* _env, _mem, _len, visited, *)
-          (* nil_env, nil_visited in *)
-      (* nil_env == [] & *)
-      (* nil_visited == [] & *)
-      (* decl == FunDecl (arg_tags, body) & *)
-      (* state == St (env_before, mem_before, len_before, visited_before) & *)
-      (* state_clean == St (nil_env, mem_before, len_before, nil_visited) & *)
-      (* list_foldr2o (add_arg_foldero state) *)
-                   (* (Std.pair state Nat.o) arg_tags args *)
-                   (* (Std.pair state_with_vars _counter) & (* TODO: or foldr2o ?? *) *)
-      (* eval_bodyo state_with_vars prog body state_evaled & *)
-      (* state_evaled == St (_env,_mem, _len, visited) & *)
-      (* state' == St (env_before, mem_before, len_before, visited) *)
-  (* } *)
+  and eval_funo state prog decl args state' =
+    let open FunDecl in
+    let open St in
+    ocanren {
+    fresh arg_tags, body,
+          env_before, mem_before, len_before, visited_before,
+          state_clean,
+          state_with_vars, _counter,
+          state_evaled,
+          _env, _mem, _len, visited,
+          nil_env, nil_visited in
+      nil_env == [] &
+      nil_visited == [] &
+      decl == FunDecl (arg_tags, body) &
+      state == St (env_before, mem_before, len_before, visited_before) &
+      state_clean == St (nil_env, mem_before, len_before, nil_visited) &
+      list_foldr2o (add_arg_foldero state)
+                   (Std.pair state Nat.o) arg_tags args
+                   (Std.pair state_with_vars _counter) & (* TODO: or foldr2o ?? *)
+      eval_bodyo state_with_vars prog body state_evaled &
+      state_evaled == St (_env,_mem, _len, visited) &
+      state' == St (env_before, mem_before, len_before, visited)
+  }
 
-  (* and eval_fun_empty_argso state prog decl state' = *)
-    (* let open FunDecl in *)
-    (* ocanren { *)
-    (* fresh arg_tags, args, _body in *)
-      (* decl == FunDecl (arg_tags, _body) & *)
-      (* List.mapo arg_to_rvalueo arg_tags args & *)
-      (* eval_funo state prog decl args state' *)
-  (* } *)
+  and eval_fun_empty_argso state prog decl state' =
+    let open FunDecl in
+    ocanren {
+    fresh arg_tags, args, _body in
+      decl == FunDecl (arg_tags, _body) &
+      List.mapo arg_to_rvalueo arg_tags args &
+      eval_funo state prog decl args state'
+  }
 
   (* --- *)
 
-  (* let empty_stateo state = *)
-    (* let open St in *)
-    (* ocanren { *)
-    (* fresh nil_env, nil_mem, nil_visited in *)
-      (* nil_env == [] & *)
-      (* nil_visited == [] & *)
-      (* nil_mem == [] & *)
-      (* state == St (nil_env, nil_mem, Nat.o, nil_visited) *)
-  (* } *)
+  let empty_stateo state =
+    let open St in
+    ocanren {
+    fresh nil_env, nil_mem, nil_visited in
+      nil_env == [] &
+      nil_visited == [] &
+      nil_mem == [] &
+      state == St (nil_env, nil_mem, Nat.o, nil_visited)
+  }
 
-  (* let eval_progo all_prog state' = *)
-    (* let open Prog in *)
-    (* ocanren { *)
-    (* fresh prog, main_decl, state in *)
-      (* all_prog == Prog (prog, main_decl) & *)
-      (* empty_stateo state & *)
-      (* eval_fun_empty_argso state prog main_decl state' *)
-  (* } *)
+  let eval_progo all_prog state' =
+    let open Prog in
+    ocanren {
+    fresh prog, main_decl, state in
+      all_prog == Prog (prog, main_decl) &
+      empty_stateo state &
+      eval_fun_empty_argso state prog main_decl state'
+  }
 end