diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml
index 50d22c6d..3ed9cdcc 100644
--- a/src/core/Sidekick_core.ml
+++ b/src/core/Sidekick_core.ml
@@ -43,5 +43,6 @@ module Proof_trace = Proof_trace
 module Proof_term = Proof_term
 module Subst = Sidekick_core_logic.Subst
 module Var = Sidekick_core_logic.Var
+module Box = Box
 
 exception Resource_exhausted
diff --git a/src/core/box.ml b/src/core/box.ml
new file mode 100644
index 00000000..f0e3cec2
--- /dev/null
+++ b/src/core/box.ml
@@ -0,0 +1,33 @@
+open Sidekick_core_logic
+
+type Const.view += Box of Term.t
+
+let ops : Const.ops =
+  (module struct
+    let pp out = function
+      | Box t -> Fmt.fprintf out "(@[box@ %a@])" Term.pp_debug t
+      | _ -> assert false
+
+    let equal a b =
+      match a, b with
+      | Box a, Box b -> Term.equal a b
+      | _ -> false
+
+    let hash = function
+      | Box t -> Hash.(combine2 10 (Term.hash t))
+      | _ -> assert false
+
+    let opaque_to_cc _ = false
+  end)
+
+let as_box t =
+  match Term.view t with
+  | Term.E_const { Const.c_view = Box u; _ } -> Some u
+  | _ -> None
+
+let box tst t : Term.t =
+  match Term.view t with
+  | Term.E_const { Const.c_view = Box _; _ } -> t
+  | _ ->
+    let c = Const.make (Box t) ~ty:(Term.ty t) ops in
+    Term.const tst c
diff --git a/src/core/box.mli b/src/core/box.mli
new file mode 100644
index 00000000..35ae893a
--- /dev/null
+++ b/src/core/box.mli
@@ -0,0 +1,9 @@
+open Sidekick_core_logic
+
+type Const.view += private Box of Term.t
+
+val box : Term.store -> Term.t -> Term.t
+(** [box tst t] makes a new constant that "boxes" [t].
+  This way it will be opaque. *)
+
+val as_box : Term.t -> Term.t option
diff --git a/src/core/t_printer.ml b/src/core/t_printer.ml
index 6edf27b9..cb4ef171 100644
--- a/src/core/t_printer.ml
+++ b/src/core/t_printer.ml
@@ -23,7 +23,15 @@ let pp_builtins_ : hook =
     true
   | _ -> false
 
-let default_ : Hooks.t = Hooks.(empty |> add pp_builtins_)
+let pp_box : hook =
+ fun ~recurse out t ->
+  match Box.as_box t with
+  | Some b ->
+    Fmt.fprintf out "[[ @[%a@] ]]" recurse b;
+    true
+  | None -> false
+
+let default_ : Hooks.t = Hooks.(empty |> add pp_builtins_ |> add pp_box)
 let default_hooks = ref default_
 
 (* debug printer *)