diff --git a/unittest/core-ast/dune b/unittest/core-ast/dune
deleted file mode 100644
index a32c666e..00000000
--- a/unittest/core-ast/dune
+++ /dev/null
@@ -1,4 +0,0 @@
-(tests
- (names t1)
- (flags :standard -open Sidekick_util)
- (libraries containers sidekick.util sidekick.core-ast))
diff --git a/unittest/core-ast/t1.ml b/unittest/core-ast/t1.ml
deleted file mode 100644
index 0afd0d19..00000000
--- a/unittest/core-ast/t1.ml
+++ /dev/null
@@ -1,58 +0,0 @@
-open Sidekick_core_ast
-
-let store = Store.create ()
-let t0 = type_ store
-let () = Fmt.printf "type0 : %a@." pp_debug t0
-let () = Fmt.printf "typeof(type0) : %a@." pp_debug (get_ty store t0)
-
-let l =
-  CCSeq.unfold (fun ty -> Some (ty, get_ty store ty)) t0
-  |> CCSeq.take 10 |> CCSeq.to_list
-
-let () = Fmt.printf "type tower: %a@." (Fmt.Dump.list pp_debug) l
-let () = assert (equal (type_ store) (type_ store))
-let bool = Str_const.const store "Bool" ~ty:(type_ store)
-let a = Str_const.const store "a" ~ty:bool
-let a' = Str_const.const store "a" ~ty:bool
-let b = Str_const.const store "b" ~ty:bool
-
-let () =
-  Fmt.printf "a: %a, b: %a, typeof(a): %a@." pp_debug a pp_debug b pp_debug
-    (ty_exn a)
-
-let () = assert (equal a a)
-let () = assert (not (equal a b))
-let ty_b2b = arrow store bool bool
-let () = Fmt.printf "b2b: %a@." pp_debug ty_b2b
-let p = Str_const.const store "p" ~ty:ty_b2b
-let q = Str_const.const store "q" ~ty:ty_b2b
-let pa = app store p a
-let pb = app store p b
-let qa = app store q a
-let qb = app store q b
-let () = Fmt.printf "p(a): %a@." pp_debug pa
-let () = Fmt.printf "p(b): %a@." pp_debug pb
-let () = Fmt.printf "q(a): %a@." pp_debug qa
-let () = Fmt.printf "q(b): %a@." pp_debug qb
-let () = assert (equal pa (app store p a))
-
-(* *)
-
-let ty_pa = ty_exn pa
-let () = Fmt.printf "typeof(p a): %a@." pp_debug ty_pa
-
-(* *)
-
-let v_x = Var.make "x" bool
-let v_y = Var.make "y" bool
-let x = var store v_x
-let y = var store v_y
-let lxy_px = lam store v_x @@ lam store v_y @@ app store p x
-
-let () =
-  Fmt.printf "@[<v2>lxy_px: %a@ type: %a@]@." pp_debug lxy_px pp_debug
-    (ty_exn lxy_px)
-
-let () =
-  let t = app_l store lxy_px [ a; b ] in
-  Fmt.printf "@[<v2>lxy_px a b: %a@ type: %a@]@." pp_debug t pp_debug (ty_exn t)
diff --git a/unittest/core-logic/dune b/unittest/core-logic/dune
new file mode 100644
index 00000000..1969c8d2
--- /dev/null
+++ b/unittest/core-logic/dune
@@ -0,0 +1,4 @@
+(tests
+ (names t1)
+ (flags :standard -open Sidekick_util)
+ (libraries containers sidekick.util sidekick.core-logic))
diff --git a/unittest/core-ast/t1.expected b/unittest/core-logic/t1.expected
similarity index 100%
rename from unittest/core-ast/t1.expected
rename to unittest/core-logic/t1.expected
diff --git a/unittest/core-logic/t1.ml b/unittest/core-logic/t1.ml
new file mode 100644
index 00000000..30f09da3
--- /dev/null
+++ b/unittest/core-logic/t1.ml
@@ -0,0 +1,59 @@
+open Sidekick_core_logic
+
+let store = Store.create ()
+let t0 = Term.type_ store
+let () = Fmt.printf "type0 : %a@." Term.pp_debug t0
+let () = Fmt.printf "typeof(type0) : %a@." Term.pp_debug (Term.get_ty store t0)
+
+let l =
+  CCSeq.unfold (fun ty -> Some (ty, Term.get_ty store ty)) t0
+  |> CCSeq.take 10 |> CCSeq.to_list
+
+let () = Fmt.printf "type tower: %a@." (Fmt.Dump.list Term.pp_debug) l
+let () = assert (Term.(equal (type_ store) (type_ store)))
+let bool = Term.const store @@ Str_const.make "Bool" ~ty:(Term.type_ store)
+let a = Term.const store @@ Str_const.make "a" ~ty:bool
+let a' = Term.const store @@ Str_const.make "a" ~ty:bool
+let b = Term.const store @@ Str_const.make "b" ~ty:bool
+
+let () =
+  Fmt.printf "a: %a, b: %a, typeof(a): %a@." Term.pp_debug a Term.pp_debug b
+    Term.pp_debug (Term.ty_exn a)
+
+let () = assert (Term.(equal a a))
+let () = assert (not Term.(equal a b))
+let ty_b2b = Term.arrow store bool bool
+let () = Fmt.printf "b2b: %a@." Term.pp_debug ty_b2b
+let p = Term.const store @@ Str_const.make "p" ~ty:ty_b2b
+let q = Term.const store @@ Str_const.make "q" ~ty:ty_b2b
+let pa = Term.app store p a
+let pb = Term.app store p b
+let qa = Term.app store q a
+let qb = Term.app store q b
+let () = Fmt.printf "p(a): %a@." Term.pp_debug pa
+let () = Fmt.printf "p(b): %a@." Term.pp_debug pb
+let () = Fmt.printf "q(a): %a@." Term.pp_debug qa
+let () = Fmt.printf "q(b): %a@." Term.pp_debug qb
+let () = assert (Term.(equal pa (app store p a)))
+
+(* *)
+
+let ty_pa = Term.ty_exn pa
+let () = Fmt.printf "typeof(p a): %a@." Term.pp_debug ty_pa
+
+(* *)
+
+let v_x = Var.make "x" bool
+let v_y = Var.make "y" bool
+let x = Term.var store v_x
+let y = Term.var store v_y
+let lxy_px = Term.lam store v_x @@ Term.lam store v_y @@ Term.app store p x
+
+let () =
+  Fmt.printf "@[<v2>lxy_px: %a@ type: %a@]@." Term.pp_debug lxy_px Term.pp_debug
+    (Term.ty_exn lxy_px)
+
+let () =
+  let t = Term.app_l store lxy_px [ a; b ] in
+  Fmt.printf "@[<v2>lxy_px a b: %a@ type: %a@]@." Term.pp_debug t Term.pp_debug
+    (Term.ty_exn t)