diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml
index e4e4ede8..fa8d7b4c 100644
--- a/src/core/Sidekick_core.ml
+++ b/src/core/Sidekick_core.ml
@@ -23,9 +23,11 @@ module Term = struct
   include Sidekick_core_logic.T_builtins
 end
 
-module Var = Sidekick_core_logic.Var
 module Bvar = Sidekick_core_logic.Bvar
-module Subst = Sidekick_core_logic.Subst
-module Proof_trace = Proof_trace
-module Proof_sat = Proof_sat
+module Lit = Lit
 module Proof_core = Proof_core
+module Proof_sat = Proof_sat
+module Proof_trace = Proof_trace
+module Proof_term = Proof_term
+module Subst = Sidekick_core_logic.Subst
+module Var = Sidekick_core_logic.Var
diff --git a/src/core/lit.ml b/src/core/lit.ml
index eb91d2da..8b85e2a4 100644
--- a/src/core/lit.ml
+++ b/src/core/lit.ml
@@ -21,6 +21,10 @@ let atom ?(sign = true) (t : term) : t =
   in
   make ~sign t
 
+let make_eq ?sign store t u : t =
+  let p = T_builtins.eq store t u in
+  atom ?sign p
+
 let equal a b = a.lit_sign = b.lit_sign && T.equal a.lit_term b.lit_term
 
 let hash a =
diff --git a/src/core/lit.mli b/src/core/lit.mli
index 25fe65e7..bf012a59 100644
--- a/src/core/lit.mli
+++ b/src/core/lit.mli
@@ -36,6 +36,8 @@ val atom : ?sign:bool -> term -> t
       its sign in the process.
       @param sign if provided, and [sign=false], negate the resulting lit. *)
 
+val make_eq : ?sign:bool -> Term.store -> term -> term -> t
+
 val norm_sign : t -> t * bool
 (** [norm_sign (+t)] is [+t, true],
       and [norm_sign (-t)] is [+t, false].