diff --git a/src/core-logic/term.ml b/src/core-logic/term.ml
index fd2cff21..5f8bd6e8 100644
--- a/src/core-logic/term.ml
+++ b/src/core-logic/term.ml
@@ -65,6 +65,11 @@ let[@inline] is_app e =
   | E_app _ -> true
   | _ -> false
 
+let[@inline] is_pi e =
+  match e.view with
+  | E_pi _ -> true
+  | _ -> false
+
 (* debug printer *)
 let expr_pp_with_ ~pp_ids ~max_depth out (e : term) : unit =
   let rec loop k ~depth names out e =
@@ -132,6 +137,8 @@ end
 module Map = CCMap.Make (AsKey)
 module Set = CCSet.Make (AsKey)
 module Tbl = CCHashtbl.Make (AsKey)
+module Weak_set = Weak.Make (AsKey)
+module Weak_map = Ephemeron.K1.Make (AsKey)
 
 module Hcons = Hashcons.Make (struct
   type nonrec t = term
diff --git a/src/core-logic/term.mli b/src/core-logic/term.mli
index adcdff02..fd6b0e4c 100644
--- a/src/core-logic/term.mli
+++ b/src/core-logic/term.mli
@@ -48,6 +48,7 @@ val pp_debug_with_ids : t Fmt.printer
 (** {2 Containers} *)
 
 include WITH_SET_MAP_TBL with type t := t
+include WITH_WEAK with type t := t
 
 (** {2 Utils} *)
 
@@ -55,6 +56,7 @@ val view : t -> view
 val unfold_app : t -> t * t list
 val is_app : t -> bool
 val is_const : t -> bool
+val is_pi : t -> bool
 
 val iter_dag : ?seen:unit Tbl.t -> iter_ty:bool -> f:(t -> unit) -> t -> unit
 (** [iter_dag t ~f] calls [f] once on each subterm of [t], [t] included.
diff --git a/src/sigs/sidekick_sigs.ml b/src/sigs/sidekick_sigs.ml
index 92e24c7f..8d9cc1e4 100644
--- a/src/sigs/sidekick_sigs.ml
+++ b/src/sigs/sidekick_sigs.ml
@@ -96,3 +96,10 @@ module type WITH_SET_MAP_TBL = sig
   module Map : CCMap.S with type key = t
   module Tbl : CCHashtbl.S with type key = t
 end
+
+module type WITH_WEAK = sig
+  type t
+
+  module Weak_set : Weak.S with type data = t
+  module Weak_map : Ephemeron.S with type key = t
+end