diff --git a/src/core-logic/Hashcons.ml b/src/core-logic/Hashcons.ml
new file mode 100644
index 00000000..28ca6e21
--- /dev/null
+++ b/src/core-logic/Hashcons.ml
@@ -0,0 +1,34 @@
+module type ARG = sig
+  type t
+
+  val equal : t -> t -> bool
+  val hash : t -> int
+  val set_id : t -> int -> unit
+end
+
+module Make (A : ARG) : sig
+  type t
+
+  val create : ?size:int -> unit -> t
+  val hashcons : t -> A.t -> A.t
+  val size : t -> int
+  val to_iter : t -> A.t Iter.t
+end = struct
+  module W = Weak.Make (A)
+
+  type t = { tbl: W.t; mutable n: int }
+
+  let create ?(size = 1024) () : t = { tbl = W.create size; n = 0 }
+
+  (* hashcons terms *)
+  let hashcons st t =
+    let t' = W.merge st.tbl t in
+    if t == t' then (
+      st.n <- 1 + st.n;
+      A.set_id t' st.n
+    );
+    t'
+
+  let size st = W.count st.tbl
+  let to_iter st yield = W.iter yield st.tbl
+end
diff --git a/src/core-logic/bvar.ml b/src/core-logic/bvar.ml
new file mode 100644
index 00000000..bddb63d7
--- /dev/null
+++ b/src/core-logic/bvar.ml
@@ -0,0 +1,9 @@
+open Types_
+
+type t = bvar = { bv_idx: int; bv_ty: term }
+
+let equal (v1 : t) v2 = v1.bv_idx = v2.bv_idx && Term_.equal v1.bv_ty v2.bv_ty
+let hash v = H.combine2 (H.int v.bv_idx) (Term_.hash v.bv_ty)
+let pp out v = Fmt.fprintf out "bv[%d]" v.bv_idx
+let[@inline] ty self = self.bv_ty
+let make i ty : t = { bv_idx = i; bv_ty = ty }
diff --git a/src/core-logic/bvar.mli b/src/core-logic/bvar.mli
new file mode 100644
index 00000000..cd1330a5
--- /dev/null
+++ b/src/core-logic/bvar.mli
@@ -0,0 +1,10 @@
+(** Bound variable *)
+
+open Types_
+
+type t = bvar = { bv_idx: int; bv_ty: term }
+
+include EQ_HASH_PRINT with type t := t
+
+val make : int -> term -> t
+val ty : t -> term
diff --git a/src/core-logic/const.ml b/src/core-logic/const.ml
new file mode 100644
index 00000000..c7004f70
--- /dev/null
+++ b/src/core-logic/const.ml
@@ -0,0 +1,29 @@
+open Types_
+
+type view = const_view = ..
+
+module type DYN_OPS = sig
+  val pp : view Fmt.printer
+  val equal : view -> view -> bool
+  val hash : view -> int
+end
+
+type ops = (module DYN_OPS)
+type t = const = { c_view: view; c_ops: ops; c_ty: term }
+
+let[@inline] view self = self.c_view
+let[@inline] ty self = self.c_ty
+
+let equal (a : t) b =
+  let (module O) = a.c_ops in
+  O.equal a.c_view b.c_view && Term_.equal a.c_ty b.c_ty
+
+let hash (a : t) : int =
+  let (module O) = a.c_ops in
+  H.combine2 (O.hash a.c_view) (Term_.hash a.c_ty)
+
+let pp out (a : t) =
+  let (module O) = a.c_ops in
+  O.pp out a.c_view
+
+let make c_view c_ops ~ty:c_ty : t = { c_view; c_ops; c_ty }
diff --git a/src/core-logic/const.mli b/src/core-logic/const.mli
new file mode 100644
index 00000000..bf22cd28
--- /dev/null
+++ b/src/core-logic/const.mli
@@ -0,0 +1,22 @@
+(** Constants.
+
+  Constants are logical symbols, defined by the user thanks to an open type *)
+
+open Types_
+
+type t = const
+type view = const_view = ..
+
+module type DYN_OPS = sig
+  val pp : view Fmt.printer
+  val equal : view -> view -> bool
+  val hash : view -> int
+end
+
+type ops = (module DYN_OPS)
+
+val view : t -> view
+val make : view -> ops -> ty:term -> t
+val ty : t -> term
+
+include EQ_HASH_PRINT with type t := t
diff --git a/src/core-logic/dune b/src/core-logic/dune
new file mode 100644
index 00000000..5b7b4f4b
--- /dev/null
+++ b/src/core-logic/dune
@@ -0,0 +1,6 @@
+(library
+ (name sidekick_core_logic)
+ (public_name sidekick.core-logic)
+ (synopsis "Core AST for logic terms and types")
+ (flags :standard -w +32 -open Sidekick_sigs -open Sidekick_util)
+ (libraries containers iter sidekick.sigs sidekick.util))
diff --git a/src/core-logic/sidekick_core_logic.ml b/src/core-logic/sidekick_core_logic.ml
new file mode 100644
index 00000000..5673f0c8
--- /dev/null
+++ b/src/core-logic/sidekick_core_logic.ml
@@ -0,0 +1,10 @@
+module Term = Term
+module Var = Var
+module Bvar = Bvar
+module Const = Const
+module Subst = Subst
+
+(* *)
+
+module Store = Term.Store
+module Str_const = Str_const
diff --git a/src/core-logic/str_const.ml b/src/core-logic/str_const.ml
new file mode 100644
index 00000000..ea92d85d
--- /dev/null
+++ b/src/core-logic/str_const.ml
@@ -0,0 +1,21 @@
+open Types_
+
+type const_view += Str of string
+
+let ops : Const.ops =
+  (module struct
+    let pp out = function
+      | Str s -> Fmt.string out s
+      | _ -> assert false
+
+    let equal a b =
+      match a, b with
+      | Str s1, Str s2 -> s1 = s2
+      | _ -> false
+
+    let hash = function
+      | Str s -> CCHash.string s
+      | _ -> assert false
+  end)
+
+let make name ~ty : Const.t = Const.make (Str name) ops ~ty
diff --git a/src/core-logic/str_const.mli b/src/core-logic/str_const.mli
new file mode 100644
index 00000000..e7cd4922
--- /dev/null
+++ b/src/core-logic/str_const.mli
@@ -0,0 +1,10 @@
+(** Basic string constants.
+
+   These constants are a string name, coupled with a type.
+*)
+
+open Types_
+
+type const_view += private Str of string
+
+val make : string -> ty:term -> const
diff --git a/src/core-logic/subst.ml b/src/core-logic/subst.ml
new file mode 100644
index 00000000..b960915a
--- /dev/null
+++ b/src/core-logic/subst.ml
@@ -0,0 +1,25 @@
+open Types_
+module M = Var_.Map
+
+type t = subst
+
+let empty = { m = M.empty }
+let is_empty self = M.is_empty self.m
+let add v t self = { m = M.add v t self.m }
+
+let pp out (self : t) =
+  if is_empty self then
+    Fmt.string out "(subst)"
+  else (
+    let pp_pair out (v, t) =
+      Fmt.fprintf out "(@[%a := %a@])" Var.pp v !Term_.pp_debug_ t
+    in
+    Fmt.fprintf out "(@[subst@ %a@])" (Util.pp_iter pp_pair) (M.to_iter self.m)
+  )
+
+let of_list l = { m = M.of_list l }
+let of_iter it = { m = M.of_iter it }
+let to_iter self = M.to_iter self.m
+
+let apply (store : Term.store) ~recursive (self : t) (e : term) : term =
+  Term.Internal_.subst_ store ~recursive e self
diff --git a/src/core-logic/subst.mli b/src/core-logic/subst.mli
new file mode 100644
index 00000000..9f88065a
--- /dev/null
+++ b/src/core-logic/subst.mli
@@ -0,0 +1,15 @@
+(** Substitutions *)
+
+open Types_
+
+type t = subst
+
+include PRINT with type t := t
+
+val empty : t
+val is_empty : t -> bool
+val of_list : (var * term) list -> t
+val of_iter : (var * term) Iter.t -> t
+val to_iter : t -> (var * term) Iter.t
+val add : var -> term -> t -> t
+val apply : Term.store -> recursive:bool -> t -> term -> term
diff --git a/src/core-logic/term.ml b/src/core-logic/term.ml
new file mode 100644
index 00000000..fe4bd9ca
--- /dev/null
+++ b/src/core-logic/term.ml
@@ -0,0 +1,618 @@
+open Types_
+
+type view = term_view =
+  | E_type of int
+  | E_var of var
+  | E_bound_var of bvar
+  | E_const of const
+  | E_app of term * term
+  | E_lam of string * term * term
+  | E_pi of string * term * term
+
+type t = term
+
+(* 5 bits in [t.id] are used to store which store it belongs to, so we have
+   a chance of detecting when the user passes a term to the wrong store *)
+let store_id_bits = 5
+
+(* mask to access the store id *)
+let store_id_mask = (1 lsl store_id_bits) - 1
+
+include Term_
+
+let[@inline] view (e : term) : view = e.view
+let[@inline] db_depth e = e.flags lsr (1 + store_id_bits)
+let[@inline] has_fvars e = (e.flags lsr store_id_bits) land 1 == 1
+let[@inline] store_uid e : int = e.flags land store_id_mask
+let[@inline] is_closed e : bool = db_depth e == 0
+
+let[@inline] ty_exn e : term =
+  match e.ty with
+  | Some x -> x
+  | None -> assert false
+
+(* open an application *)
+let unfold_app (e : term) : term * term list =
+  let[@unroll 1] rec aux acc e =
+    match e.view with
+    | E_app (f, a) -> aux (a :: acc) f
+    | _ -> e, acc
+  in
+  aux [] e
+
+(* debug printer *)
+let expr_pp_with_ ~pp_ids ~max_depth out (e : term) : unit =
+  let rec loop k ~depth names out e =
+    let pp' = loop' k ~depth:(depth + 1) names in
+    (match e.view with
+    | E_type 0 -> Fmt.string out "type"
+    | E_type i -> Fmt.fprintf out "type_%d" i
+    | E_var v -> Fmt.string out v.v_name
+    (* | E_var v -> Fmt.fprintf out "(@[%s : %a@])" v.v_name pp v.v_ty *)
+    | E_bound_var v ->
+      let idx = v.bv_idx in
+      (match CCList.nth_opt names idx with
+      | Some n when n <> "" -> Fmt.string out n
+      | _ ->
+        if idx < k then
+          Fmt.fprintf out "x_%d" (k - idx - 1)
+        else
+          Fmt.fprintf out "%%db_%d" (idx - k))
+    | E_const c -> Const.pp out c
+    | (E_app _ | E_lam _) when depth > max_depth ->
+      Fmt.fprintf out "@<1>…/%d" e.id
+    | E_app _ ->
+      let f, args = unfold_app e in
+      Fmt.fprintf out "%a@ %a" pp' f (Util.pp_list pp') args
+    | E_lam ("", _ty, bod) ->
+      Fmt.fprintf out "(@[\\x_%d:@[%a@].@ %a@])" k pp' _ty
+        (loop (k + 1) ~depth:(depth + 1) ("" :: names))
+        bod
+    | E_lam (n, _ty, bod) ->
+      Fmt.fprintf out "(@[\\%s:@[%a@].@ %a@])" n pp' _ty
+        (loop (k + 1) ~depth:(depth + 1) (n :: names))
+        bod
+    | E_pi (_, ty, bod) when is_closed bod ->
+      (* actually just an arrow *)
+      Fmt.fprintf out "(@[%a@ -> %a@])"
+        (loop k ~depth:(depth + 1) names)
+        ty
+        (loop (k + 1) ~depth:(depth + 1) ("" :: names))
+        bod
+    | E_pi ("", _ty, bod) ->
+      Fmt.fprintf out "(@[Pi x_%d:@[%a@].@ %a@])" k pp' _ty
+        (loop (k + 1) ~depth:(depth + 1) ("" :: names))
+        bod
+    | E_pi (n, _ty, bod) ->
+      Fmt.fprintf out "(@[Pi %s:@[%a@].@ %a@])" n pp' _ty
+        (loop (k + 1) ~depth:(depth + 1) (n :: names))
+        bod);
+    if pp_ids then Fmt.fprintf out "/%d" e.id
+  and loop' k ~depth names out e =
+    match e.view with
+    | E_type _ | E_var _ | E_bound_var _ | E_const _ ->
+      loop k ~depth names out e (* atomic expr *)
+    | E_app _ | E_lam _ | E_pi _ ->
+      Fmt.fprintf out "(%a)" (loop k ~depth names) e
+  in
+  Fmt.fprintf out "@[%a@]" (loop 0 ~depth:0 []) e
+
+let pp_debug = expr_pp_with_ ~pp_ids:false ~max_depth:max_int
+let pp_debug_with_ids = expr_pp_with_ ~pp_ids:true ~max_depth:max_int
+let () = pp_debug_ := pp_debug
+
+module AsKey = struct
+  type nonrec t = term
+
+  let equal = equal
+  let compare = compare
+  let hash = hash
+end
+
+module Map = CCMap.Make (AsKey)
+module Set = CCSet.Make (AsKey)
+module Tbl = CCHashtbl.Make (AsKey)
+
+module Hcons = Hashcons.Make (struct
+  type nonrec t = term
+
+  let equal a b =
+    match a.view, b.view with
+    | E_type i, E_type j -> i = j
+    | E_const c1, E_const c2 -> Const.equal c1 c2
+    | E_var v1, E_var v2 -> Var.equal v1 v2
+    | E_bound_var v1, E_bound_var v2 -> Bvar.equal v1 v2
+    | E_app (f1, a1), E_app (f2, a2) -> equal f1 f2 && equal a1 a2
+    | E_lam (_, ty1, bod1), E_lam (_, ty2, bod2) ->
+      equal ty1 ty2 && equal bod1 bod2
+    | ( ( E_type _ | E_const _ | E_var _ | E_bound_var _ | E_app _ | E_lam _
+        | E_pi _ ),
+        _ ) ->
+      false
+
+  let hash e : int =
+    match e.view with
+    | E_type i -> H.combine2 10 (H.int i)
+    | E_const c -> H.combine2 20 (Const.hash c)
+    | E_var v -> H.combine2 30 (Var.hash v)
+    | E_bound_var v -> H.combine2 40 (Bvar.hash v)
+    | E_app (f, a) -> H.combine3 50 (hash f) (hash a)
+    | E_lam (_, ty, bod) -> H.combine3 60 (hash ty) (hash bod)
+    | E_pi (_, ty, bod) -> H.combine3 70 (hash ty) (hash bod)
+
+  let set_id t id =
+    assert (t.id == -1);
+    t.id <- id
+end)
+
+module Store = struct
+  type t = { (* unique ID for this store *)
+             s_uid: int; s_exprs: Hcons.t }
+
+  (* TODO: use atomic? CCAtomic? *)
+  let n = ref 0
+
+  let create () : t =
+    let s_uid = !n in
+    incr n;
+    { s_uid; s_exprs = Hcons.create ~size:256 () }
+
+  (* check that [e] belongs in this store *)
+  let[@inline] check_e_uid (self : t) (e : term) =
+    assert (self.s_uid == store_uid e)
+end
+
+type store = Store.t
+
+let iter_shallow ~f (e : term) : unit =
+  match e.view with
+  | E_type _ -> ()
+  | _ ->
+    (match e.ty with
+    | None -> (* should be computed at build time *) assert false
+    | Some ty -> f false ty);
+    (match e.view with
+    | E_const _ -> ()
+    | E_type _ -> assert false
+    | E_var v -> f false v.v_ty
+    | E_bound_var v -> f false v.bv_ty
+    | E_app (hd, a) ->
+      f false hd;
+      f false a
+    | E_lam (_, tyv, bod) | E_pi (_, tyv, bod) ->
+      f false tyv;
+      f true bod)
+
+let map_shallow_ ~make ~f (e : term) : term =
+  match view e with
+  | E_type _ | E_const _ -> e
+  | E_var v ->
+    let v_ty = f false v.v_ty in
+    if v_ty == v.v_ty then
+      e
+    else
+      make (E_var { v with v_ty })
+  | E_bound_var v ->
+    let ty' = f false v.bv_ty in
+    if v.bv_ty == ty' then
+      e
+    else
+      make (E_bound_var { v with bv_ty = ty' })
+  | E_app (hd, a) ->
+    let hd' = f false hd in
+    let a' = f false a in
+    if a == a' && hd == hd' then
+      e
+    else
+      make (E_app (f false hd, f false a))
+  | E_lam (n, tyv, bod) ->
+    let tyv' = f false tyv in
+    let bod' = f true bod in
+    if tyv == tyv' && bod == bod' then
+      e
+    else
+      make (E_lam (n, tyv', bod'))
+  | E_pi (n, tyv, bod) ->
+    let tyv' = f false tyv in
+    let bod' = f true bod in
+    if tyv == tyv' && bod == bod' then
+      e
+    else
+      make (E_pi (n, tyv', bod'))
+
+(* TODO
+   (* map immediate subterms *)
+   let map_shallow ctx ~f (e : t) : t =
+     match view e with
+     | E_kind | E_type | E_const (_, []) | E_box _ -> e
+     | _ ->
+       let ty' =
+         lazy
+           (match e.e_ty with
+           | (lazy None) -> None
+           | (lazy (Some ty)) -> Some (f false ty))
+       in
+       (match view e with
+       | E_var v ->
+         let v_ty = f false v.v_ty in
+         if v_ty == v.v_ty then
+           e
+         else
+           make_ ctx (E_var { v with v_ty }) ty'
+       | E_const (c, args) ->
+         let args' = List.map (f false) args in
+         if List.for_all2 equal args args' then
+           e
+         else
+           make_ ctx (E_const (c, args')) ty'
+       | E_bound_var v ->
+         let ty' = f false v.bv_ty in
+         if v.bv_ty == ty' then
+           e
+         else
+           make_ ctx
+             (E_bound_var { v with bv_ty = ty' })
+             (Lazy.from_val (Some ty'))
+       | E_app (hd, a) ->
+         let hd' = f false hd in
+         let a' = f false a in
+         if a == a' && hd == hd' then
+           e
+         else
+           make_ ctx (E_app (f false hd, f false a)) ty'
+       | E_lam (n, tyv, bod) ->
+         let tyv' = f false tyv in
+         let bod' = f true bod in
+         if tyv == tyv' && bod == bod' then
+           e
+         else
+           make_ ctx (E_lam (n, tyv', bod')) ty'
+       | E_arrow (a, b) ->
+         let a' = f false a in
+         let b' = f false b in
+         if a == a' && b == b' then
+           e
+         else
+           make_ ctx (E_arrow (a', b')) ty'
+       | E_kind | E_type | E_box _ -> assert false)
+*)
+
+exception IsSub
+
+let[@inline] is_type_ e =
+  match e.view with
+  | E_type _ -> true
+  | _ -> false
+
+let[@inline] is_a_type e = is_type_ e || is_type_ (ty_exn e)
+
+let iter_dag ?(seen = Tbl.create 8) ~iter_ty ~f e : unit =
+  let rec loop e =
+    if not (Tbl.mem seen e) then (
+      Tbl.add seen e ();
+      if iter_ty && not (is_type_ e) then loop (ty_exn e);
+      f e;
+      iter_shallow e ~f:(fun _ u -> loop u)
+    )
+  in
+  loop e
+
+exception E_exit
+
+let exists_shallow ~f e : bool =
+  try
+    iter_shallow e ~f:(fun b x -> if f b x then raise_notrace E_exit);
+    false
+  with E_exit -> true
+
+let for_all_shallow ~f e : bool =
+  try
+    iter_shallow e ~f:(fun b x -> if not (f b x) then raise_notrace E_exit);
+    true
+  with E_exit -> false
+
+let contains e ~sub : bool =
+  try
+    iter_dag ~iter_ty:true e ~f:(fun e' ->
+        if equal e' sub then raise_notrace IsSub);
+    false
+  with IsSub -> true
+
+let free_vars_iter e : var Iter.t =
+ fun yield ->
+  iter_dag ~iter_ty:true e ~f:(fun e' ->
+      match view e' with
+      | E_var v -> yield v
+      | _ -> ())
+
+let free_vars ?(init = Var.Set.empty) e : Var.Set.t =
+  let set = ref init in
+  free_vars_iter e (fun v -> set := Var.Set.add v !set);
+  !set
+
+module Make_ = struct
+  let compute_db_depth_ e : int =
+    if is_type_ e then
+      0
+    else (
+      let d1 = db_depth @@ ty_exn e in
+      let d2 =
+        match view e with
+        | E_type _ | E_const _ | E_var _ -> 0
+        | E_bound_var v -> v.bv_idx + 1
+        | E_app (a, b) -> max (db_depth a) (db_depth b)
+        | E_lam (_, ty, bod) | E_pi (_, ty, bod) ->
+          max (db_depth ty) (max 0 (db_depth bod - 1))
+      in
+      max d1 d2
+    )
+
+  let compute_has_fvars_ e : bool =
+    if is_type_ e then
+      false
+    else
+      has_fvars (ty_exn e)
+      ||
+      match view e with
+      | E_var _ -> true
+      | E_type _ | E_bound_var _ | E_const _ -> false
+      | E_app (a, b) -> has_fvars a || has_fvars b
+      | E_lam (_, ty, bod) | E_pi (_, ty, bod) -> has_fvars ty || has_fvars bod
+
+  let universe_ (e : term) : int =
+    match e.view with
+    | E_type i -> i
+    | _ -> assert false
+
+  let[@inline] universe_of_ty_ (e : term) : int =
+    match e.view with
+    | E_type i -> i + 1
+    | _ -> universe_ (ty_exn e)
+
+  module T_int_tbl = CCHashtbl.Make (struct
+    type t = term * int
+
+    let equal (t1, k1) (t2, k2) = equal t1 t2 && k1 == k2
+    let hash (t, k) = H.combine3 27 (hash t) (H.int k)
+  end)
+
+  let db_shift_ ~make (e : term) (n : int) =
+    let rec loop e k : term =
+      if is_closed e then
+        e
+      else if is_a_type e then
+        e
+      else (
+        match view e with
+        | E_bound_var bv ->
+          if bv.bv_idx >= k then
+            make (E_bound_var (Bvar.make (bv.bv_idx + n) bv.bv_ty))
+          else
+            e
+        | _ ->
+          map_shallow_ e ~make ~f:(fun inbind u ->
+              loop u
+                (if inbind then
+                  k + 1
+                else
+                  k))
+      )
+    in
+    assert (n >= 0);
+    if n = 0 || is_closed e then
+      e
+    else
+      loop e 0
+
+  (* replace DB0 in [e] with [u] *)
+  let db_0_replace_ ~make e ~by:u : term =
+    let cache_ = T_int_tbl.create 8 in
+
+    let rec aux e k : term =
+      if is_a_type e then
+        e
+      else if db_depth e < k then
+        e
+      else (
+        match view e with
+        | E_const _ -> e
+        | E_bound_var bv when bv.bv_idx = k ->
+          (* replace here *)
+          db_shift_ ~make u k
+        | _ ->
+          (* use the cache *)
+          (try T_int_tbl.find cache_ (e, k)
+           with Not_found ->
+             let r =
+               map_shallow_ e ~make ~f:(fun inb u ->
+                   aux u
+                     (if inb then
+                       k + 1
+                     else
+                       k))
+             in
+             T_int_tbl.add cache_ (e, k) r;
+             r)
+      )
+    in
+    if is_closed e then
+      e
+    else
+      aux e 0
+
+  let subst_ ~make ~recursive e0 (subst : subst) : t =
+    (* cache for types and some terms *)
+    let cache_ = T_int_tbl.create 16 in
+
+    let rec loop k e =
+      try T_int_tbl.find cache_ (e, k)
+      with Not_found ->
+        let r = loop_uncached_ k e in
+        T_int_tbl.add cache_ (e, k) r;
+        r
+    and loop_uncached_ k (e : t) : t =
+      match view e with
+      | _ when not (has_fvars e) -> e (* nothing to subst in *)
+      | E_var v ->
+        (* first, subst in type *)
+        let v = { v with v_ty = loop k v.v_ty } in
+        (match Var_.Map.find v subst.m with
+        | u ->
+          let u = db_shift_ ~make u k in
+          if recursive then
+            loop 0 u
+          else
+            u
+        | exception Not_found -> make (E_var v))
+      | E_const _ -> e
+      | _ ->
+        map_shallow_ e ~make ~f:(fun inb u ->
+            loop
+              (if inb then
+                k + 1
+              else
+                k)
+              u)
+    in
+
+    if Var_.Map.is_empty subst.m then
+      e0
+    else
+      loop 0 e0
+
+  let compute_ty_ ~make (view : view) : term =
+    match view with
+    | E_var v -> Var.ty v
+    | E_bound_var v -> Bvar.ty v
+    | E_type i -> make (E_type (i + 1))
+    | E_const c -> Const.ty c
+    | E_lam (name, ty, bod) ->
+      (* type of [\x:tau. bod] is [pi x:tau. typeof(bod)] *)
+      let ty_bod = ty_exn bod in
+      make (E_pi (name, ty, ty_bod))
+    | E_app (f, a) ->
+      (* type of [f a], where [a:tau] and [f: Pi x:tau. ty_bod_f],
+         is [ty_bod_f[x := a]] *)
+      let ty_f = ty_exn f in
+      let ty_a = ty_exn a in
+      (match ty_f.view with
+      | E_pi (_, ty_arg_f, ty_bod_f) ->
+        (* check that the expected type matches *)
+        if not (equal ty_arg_f ty_a) then
+          Error.errorf
+            "@[<2>cannot apply %a to %a,@ expected argument type: %a@ actual: \
+             %a@]"
+            pp_debug f pp_debug a pp_debug ty_arg_f pp_debug ty_a;
+        db_0_replace_ ~make ty_bod_f ~by:a
+      | _ ->
+        Error.errorf
+          "@[<2>cannot apply %a,@ must have Pi type, but actual type is %a@]"
+          pp_debug f pp_debug ty_f)
+    | E_pi (_, ty, bod) ->
+      (* TODO: check the actual triplets for COC *)
+      Fmt.printf "pi %a %a@." pp_debug ty pp_debug bod;
+      let u = max (universe_of_ty_ ty) (universe_of_ty_ bod) + 1 in
+      make (E_type u)
+
+  (* hashconsing + computing metadata + computing type (for new terms) *)
+  let rec make_ (store : store) view : term =
+    let e = { view; ty = None; id = -1; flags = 0 } in
+    let e2 = Hcons.hashcons store.s_exprs e in
+    if e == e2 then (
+      (* new term, compute metadata *)
+      assert (store.s_uid land store_id_mask == store.s_uid);
+
+      (* first, compute type *)
+      if not (is_type_ e) then (
+        let ty = compute_ty_ ~make:(make_ store) view in
+        e.ty <- Some ty
+      );
+      let has_fvars = compute_has_fvars_ e in
+      e2.flags <-
+        (compute_db_depth_ e lsl (1 + store_id_bits))
+        lor (if has_fvars then
+              1 lsl store_id_bits
+            else
+              0)
+        lor store.s_uid;
+      Store.check_e_uid store e2
+    );
+    e2
+
+  let type_of_univ store i : term = make_ store (E_type i)
+  let type_ store : term = type_of_univ store 0
+  let var store v : term = make_ store (E_var v)
+  let var_str store name ~ty : term = var store (Var.make name ty)
+  let bvar store v : term = make_ store (E_bound_var v)
+  let const store c : term = make_ store (E_const c)
+  let app store f a = make_ store (E_app (f, a))
+  let app_l store f l = List.fold_left (app store) f l
+
+  let abs_on_ (store : store) (v : var) (e : term) : term =
+    Store.check_e_uid store v.v_ty;
+    Store.check_e_uid store e;
+    if not (is_closed v.v_ty) then
+      Error.errorf "cannot abstract on variable@ with non closed type %a"
+        pp_debug v.v_ty;
+    let db0 = bvar store (Bvar.make 0 v.v_ty) in
+    let body = db_shift_ ~make:(make_ store) e 1 in
+    subst_ ~make:(make_ store) ~recursive:false body
+      { m = Var_.Map.singleton v db0 }
+
+  let lam store v bod : term =
+    let bod' = abs_on_ store v bod in
+    make_ store (E_lam (Var.name v, Var.ty v, bod'))
+
+  let pi store v bod : term =
+    let bod' = abs_on_ store v bod in
+    make_ store (E_pi (Var.name v, Var.ty v, bod'))
+
+  let arrow store a b : term =
+    let b' = db_shift_ ~make:(make_ store) b 1 in
+    make_ store (E_pi ("", a, b'))
+
+  let arrow_l store args ret = List.fold_right (arrow store) args ret
+
+  (* find a name that doesn't capture a variable of [e] *)
+  let pick_name_ (name0 : string) (e : term) : string =
+    let rec loop i =
+      let name =
+        if i = 0 then
+          name0
+        else
+          Printf.sprintf "%s%d" name0 i
+      in
+      if free_vars_iter e |> Iter.exists (fun v -> v.v_name = name) then
+        loop (i + 1)
+      else
+        name
+    in
+    loop 0
+
+  let open_lambda store e : _ option =
+    match view e with
+    | E_lam (name, ty, bod) ->
+      let name = pick_name_ name bod in
+      let v = Var.make name ty in
+      let bod' = db_0_replace_ bod ~make:(make_ store) ~by:(var store v) in
+      Some (v, bod')
+    | _ -> None
+
+  let open_lambda_exn store e =
+    match open_lambda store e with
+    | Some tup -> tup
+    | None -> Error.errorf "open-lambda: term is not a lambda:@ %a" pp_debug e
+end
+
+include Make_
+
+let get_ty store e : term =
+  match e.view with
+  | E_type i -> type_of_univ store (i + 1)
+  | _ -> ty_exn e
+
+(* re-export some internal things *)
+module Internal_ = struct
+  let subst_ store ~recursive t subst =
+    subst_ ~make:(make_ store) ~recursive t subst
+end
diff --git a/src/core-logic/term.mli b/src/core-logic/term.mli
new file mode 100644
index 00000000..24d4382d
--- /dev/null
+++ b/src/core-logic/term.mli
@@ -0,0 +1,103 @@
+(** Core logic terms.
+
+  The core terms are expressions in the calculus of constructions,
+  with no universe polymorphism nor cumulativity. It should be fast, with hashconsing;
+  and simple enough (no inductives, no universe trickery).
+
+  It is intended to be the foundation for user-level terms and types and formulas.
+*)
+
+open Types_
+
+type t = term
+(** A term, in the calculus of constructions *)
+
+type store
+(** The store for terms.
+
+    The store is responsible for allocating unique IDs to terms, and
+    enforcing their hashconsing (so that syntactic equality is just a pointer
+    comparison). *)
+
+(** View.
+
+    A view is the shape of the root node of a term. *)
+type view = term_view =
+  | E_type of int
+  | E_var of var
+  | E_bound_var of bvar
+  | E_const of const
+  | E_app of t * t
+  | E_lam of string * t * t
+  | E_pi of string * t * t
+
+include EQ_ORD_HASH with type t := t
+
+val pp_debug : t Fmt.printer
+val pp_debug_with_ids : t Fmt.printer
+
+(** {2 Containers} *)
+
+include WITH_SET_MAP_TBL with type t := t
+
+(** {2 Utils} *)
+
+val view : t -> view
+val unfold_app : t -> t * t list
+val iter_dag : ?seen:unit Tbl.t -> iter_ty:bool -> f:(t -> unit) -> t -> unit
+
+val iter_shallow : f:(bool -> t -> unit) -> t -> unit
+(** [iter_shallow f e] iterates on immediate subterms of [e],
+  calling [f trdb e'] for each subterm [e'], with [trdb = true] iff
+  [e'] is directly under a binder. *)
+
+val exists_shallow : f:(bool -> t -> bool) -> t -> bool
+val for_all_shallow : f:(bool -> t -> bool) -> t -> bool
+val contains : t -> sub:t -> bool
+val free_vars_iter : t -> var Iter.t
+val free_vars : ?init:Var.Set.t -> t -> Var.Set.t
+
+val is_closed : t -> bool
+(** Is the term closed (all bound variables are paired with a binder)?
+ time: O(1) *)
+
+val has_fvars : t -> bool
+(** Does the term contain free variables?
+  time: O(1)  *)
+
+val ty_exn : t -> t
+(** Return the type of this term. Fails if the term is a type. *)
+
+val get_ty : store -> t -> t
+(** [get_ty store t] gets the type of [t], or computes it on demand
+    in case [t] is itself a type. *)
+
+(** {2 Creation} *)
+
+module Store : sig
+  type t = store
+
+  val create : unit -> t
+end
+
+val type_ : store -> t
+val type_of_univ : store -> int -> t
+val var : store -> var -> t
+val var_str : store -> string -> ty:t -> t
+val const : store -> Const.t -> t
+val app : store -> t -> t -> t
+val app_l : store -> t -> t list -> t
+val lam : store -> var -> t -> t
+val pi : store -> var -> t -> t
+val arrow : store -> t -> t -> t
+val arrow_l : store -> t list -> t -> t
+val open_lambda : store -> t -> (var * t) option
+val open_lambda_exn : store -> t -> var * t
+
+(**/**)
+
+module Internal_ : sig
+  val subst_ : store -> recursive:bool -> t -> subst -> t
+end
+
+(**/**)
diff --git a/src/core-logic/types_.ml b/src/core-logic/types_.ml
new file mode 100644
index 00000000..f62a5922
--- /dev/null
+++ b/src/core-logic/types_.ml
@@ -0,0 +1,67 @@
+module H = CCHash
+
+type const_view = ..
+
+module type DYN_CONST_OPS = sig
+  val pp : const_view Fmt.printer
+  val equal : const_view -> const_view -> bool
+  val hash : const_view -> int
+end
+
+type const_ops = (module DYN_CONST_OPS)
+
+type term_view =
+  | E_type of int
+  | E_var of var
+  | E_bound_var of bvar
+  | E_const of const
+  | E_app of term * term
+  | E_lam of string * term * term
+  | E_pi of string * term * term
+
+and var = { v_name: string; v_ty: term }
+and bvar = { bv_idx: int; bv_ty: term }
+and const = { c_view: const_view; c_ops: const_ops; c_ty: term }
+
+and term = {
+  view: term_view;
+  (* computed on demand *)
+  mutable ty: term option;
+  mutable id: int;
+  (* contains: [highest DB var | 1:has free vars | 5:ctx uid] *)
+  mutable flags: int;
+}
+
+module Term_ = struct
+  let[@inline] equal (e1 : term) e2 : bool = e1 == e2
+  let[@inline] hash (e : term) = H.int e.id
+  let[@inline] compare (e1 : term) e2 : int = CCInt.compare e1.id e2.id
+  let pp_debug_ : term Fmt.printer ref = ref (fun _ _ -> assert false)
+end
+
+module Var_ = struct
+  let[@inline] equal v1 v2 =
+    v1.v_name = v2.v_name && Term_.equal v1.v_ty v2.v_ty
+
+  let[@inline] hash v1 = H.combine3 5 (H.string v1.v_name) (Term_.hash v1.v_ty)
+
+  let compare a b : int =
+    if Term_.equal a.v_ty b.v_ty then
+      String.compare a.v_name b.v_name
+    else
+      compare a.v_ty b.v_ty
+
+  module AsKey = struct
+    type nonrec t = var
+
+    let equal = equal
+    let compare = compare
+    let hash = hash
+  end
+
+  module Map = CCMap.Make (AsKey)
+  module Set = CCSet.Make (AsKey)
+  module Tbl = CCHashtbl.Make (AsKey)
+end
+
+type subst = { m: term Var_.Map.t } [@@unboxed]
diff --git a/src/core-logic/var.ml b/src/core-logic/var.ml
new file mode 100644
index 00000000..492962a1
--- /dev/null
+++ b/src/core-logic/var.ml
@@ -0,0 +1,14 @@
+open Types_
+
+type t = var = { v_name: string; v_ty: term }
+
+include Var_
+
+let[@inline] name v = v.v_name
+let[@inline] ty self = self.v_ty
+let[@inline] pp out v1 = Fmt.string out v1.v_name
+let make v_name v_ty : t = { v_name; v_ty }
+let makef fmt ty = Fmt.kasprintf (fun s -> make s ty) fmt
+
+let pp_with_ty out v =
+  Fmt.fprintf out "(@[%s :@ %a@])" v.v_name !Term_.pp_debug_ v.v_ty
diff --git a/src/core-logic/var.mli b/src/core-logic/var.mli
new file mode 100644
index 00000000..3b3bdee8
--- /dev/null
+++ b/src/core-logic/var.mli
@@ -0,0 +1,15 @@
+(** Free variable *)
+
+open Types_
+
+type t = var = { v_name: string; v_ty: term }
+
+include EQ_ORD_HASH_PRINT with type t := t
+
+val pp_with_ty : t Fmt.printer
+val make : string -> term -> t
+val makef : ('a, Format.formatter, unit, t) format4 -> term -> 'a
+val name : t -> string
+val ty : t -> term
+
+include WITH_SET_MAP_TBL with type t := t