diff --git a/sledge/src/trm.ml b/sledge/src/trm.ml
index ef9bf4204..381ccf61b 100644
--- a/sledge/src/trm.ml
+++ b/sledge/src/trm.ml
@@ -18,6 +18,7 @@ module rec Var : sig
   include Ses.Var_intf.VAR with type t = private Trm.t
 
   val of_ : Trm.t -> t
+  val of_trm : Trm.t -> t option
 end = struct
   module T = struct
     type t = Trm.t [@@deriving compare, equal, sexp]
@@ -36,6 +37,7 @@ end = struct
   include Ses.Var0.Make (T)
 
   let of_ v = v |> check T.invariant
+  let of_trm = function Trm.Var _ as v -> Some v | _ -> None
 end
 
 and Arith0 :
diff --git a/sledge/src/trm.mli b/sledge/src/trm.mli
index e178734ed..f9b453b6b 100644
--- a/sledge/src/trm.mli
+++ b/sledge/src/trm.mli
@@ -36,6 +36,7 @@ module Var : sig
   include Ses.Var_intf.VAR with type t = private trm
 
   val of_ : trm -> t
+  val of_trm : trm -> t option
 end
 
 module Arith :