diff --git a/src/cc/Sidekick_cc.ml b/src/cc/Sidekick_cc.ml
index 66ec066a..3d1c5443 100644
--- a/src/cc/Sidekick_cc.ml
+++ b/src/cc/Sidekick_cc.ml
@@ -832,6 +832,9 @@ module Make(CC_A: ARG) = struct
       (fun k->k "(@[cc.theory.merge@ :n1 %a@ :n2 %a@ :expl %a@])" N.pp n1 N.pp n2 Expl.pp expl);
     merge_classes cc n1 n2 expl
 
+  let[@inline] merge_t cc t1 t2 expl =
+    merge cc (add_term cc t1) (add_term cc t2) expl
+
   let on_merge cc f = cc.on_merge <- f :: cc.on_merge
   let on_new_term cc f = cc.on_new_term <- f :: cc.on_new_term
   let on_conflict cc f = cc.on_conflict <- f :: cc.on_conflict
diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml
index 37c1c453..b508c856 100644
--- a/src/core/Sidekick_core.ml
+++ b/src/core/Sidekick_core.ml
@@ -273,6 +273,9 @@ module type CC_S = sig
       It must be a theory tautology that [expl ==> n1 = n2].
       To be used in theories. *)
 
+  val merge_t : t -> term -> term -> Expl.t -> unit
+  (** Shortcut for adding + merging *)
+
   val check : t -> actions -> unit
   (** Perform all pending operations done via {!assert_eq}, {!assert_lit}, etc.
       Will use the {!actions} to propagate literals, declare conflicts, etc. *)