diff --git a/sledge/src/arithmetic_intf.ml b/sledge/src/arithmetic_intf.ml
index 3fc4cd652..e066d12b8 100644
--- a/sledge/src/arithmetic_intf.ml
+++ b/sledge/src/arithmetic_intf.ml
@@ -7,14 +7,12 @@
 
 (** Arithmetic terms *)
 
-module Var = Ses.Var
-
 module type S = sig
   type var
   type trm
   type t [@@deriving compare, equal, sexp]
 
-  val ppx : var Var.strength -> t pp
+  val ppx : var Ses.Var_intf.strength -> t pp
 
   (** Construct and Destruct atomic terms *)
 
@@ -89,7 +87,7 @@ module type INDETERMINATE = sig
   type trm [@@deriving compare, equal, sexp]
   type var
 
-  val ppx : var Var.strength -> trm pp
+  val ppx : var Ses.Var_intf.strength -> trm pp
   val pp : trm pp
   val vars : trm -> var iter
 end
diff --git a/sledge/src/fml.mli b/sledge/src/fml.mli
index df8863a54..2099a6bea 100644
--- a/sledge/src/fml.mli
+++ b/sledge/src/fml.mli
@@ -33,7 +33,7 @@ module Set : sig
   val t_of_sexp : Sexp.t -> t
 end
 
-val ppx : Var.t Var.strength -> t pp
+val ppx : Var.strength -> t pp
 val pp : t pp
 
 (** Construct *)
diff --git a/sledge/src/fol.mli b/sledge/src/fol.mli
index 2299c0c99..e351510c9 100644
--- a/sledge/src/fol.mli
+++ b/sledge/src/fol.mli
@@ -10,7 +10,7 @@ module rec Term : sig
   type t [@@deriving compare, equal, sexp]
 
   (* pretty-printing *)
-  val ppx : Var.t Var.strength -> t pp
+  val ppx : Var.strength -> t pp
   val pp : t pp
 
   module Map : Map.S with type key := t
@@ -88,7 +88,7 @@ and Formula : sig
   val project : Term.t -> t option
 
   (* pretty-printing *)
-  val ppx : Var.t Var.strength -> t pp
+  val ppx : Var.strength -> t pp
   val pp : t pp
 
   (** Construct *)
@@ -147,7 +147,7 @@ module Context : sig
   val pp : t pp
 
   val ppx_diff :
-    Var.t Var.strength -> Format.formatter -> t -> Formula.t -> t -> bool
+    Var.strength -> Format.formatter -> t -> Formula.t -> t -> bool
 
   include Invariant.S with type t := t
 
diff --git a/sledge/src/ses/equality.mli b/sledge/src/ses/equality.mli
index 6e826038a..68f2f100c 100644
--- a/sledge/src/ses/equality.mli
+++ b/sledge/src/ses/equality.mli
@@ -22,7 +22,7 @@ val classes : t -> classes
 
 val pp : t pp
 val pp_classes : t pp
-val ppx_classes : Var.t Var.strength -> classes pp
+val ppx_classes : Var.strength -> classes pp
 
 include Invariant.S with type t := t
 
diff --git a/sledge/src/ses/term.mli b/sledge/src/ses/term.mli
index 6cc295367..2c0a06e12 100644
--- a/sledge/src/ses/term.mli
+++ b/sledge/src/ses/term.mli
@@ -106,7 +106,7 @@ module Map : sig
   val t_of_sexp : (Sexp.t -> 'a) -> Sexp.t -> 'a t
 end
 
-val ppx : Var.t Var.strength -> t pp
+val ppx : Var.strength -> t pp
 val pp : t pp
 val pp_diff : (t * t) pp
 val invariant : t -> unit
diff --git a/sledge/src/ses/var0.ml b/sledge/src/ses/var0.ml
index 781417e85..1ef6193fb 100644
--- a/sledge/src/ses/var0.ml
+++ b/sledge/src/ses/var0.ml
@@ -11,7 +11,7 @@ open Var_intf
 module Make (T : REPR) = struct
   include T
 
-  type 'a strength = 'a -> [`Universal | `Existential | `Anonymous] option
+  type nonrec strength = t strength
 
   let ppx strength ppf v =
     let id = id v in
diff --git a/sledge/src/ses/var_intf.ml b/sledge/src/ses/var_intf.ml
index 3c5fbe974..4e6d8d16c 100644
--- a/sledge/src/ses/var_intf.ml
+++ b/sledge/src/ses/var_intf.ml
@@ -13,11 +13,13 @@ module type REPR = sig
   val name : t -> string
 end
 
+type 'a strength = 'a -> [`Universal | `Existential | `Anonymous] option
+
 module type VAR = sig
   type t [@@deriving compare, equal, sexp]
-  type 'a strength = 'a -> [`Universal | `Existential | `Anonymous] option
+  type nonrec strength = t strength
 
-  val ppx : t strength -> t pp
+  val ppx : strength -> t pp
   val pp : t pp
 
   module Map : sig
@@ -27,13 +29,11 @@ module type VAR = sig
   end
 
   module Set : sig
-    type var := t
-
     include NS.Set.S with type elt := t
 
     val sexp_of_t : t -> Sexp.t
     val t_of_sexp : Sexp.t -> t
-    val ppx : var strength -> t pp
+    val ppx : strength -> t pp
     val pp : t pp
     val pp_xs : t pp
   end
diff --git a/sledge/src/trm.ml b/sledge/src/trm.ml
index baed849ca..92daf7b49 100644
--- a/sledge/src/trm.ml
+++ b/sledge/src/trm.ml
@@ -89,7 +89,7 @@ and Trm : sig
     | Apply of Funsym.t * t array
   [@@deriving compare, equal, sexp]
 
-  val ppx : Var.t Var.strength -> t pp
+  val ppx : Var.strength -> t pp
   val pp : t pp
   val _Var : int -> string -> t
   val _Z : Z.t -> t
diff --git a/sledge/src/trm.mli b/sledge/src/trm.mli
index b341b7d3c..10a8ca329 100644
--- a/sledge/src/trm.mli
+++ b/sledge/src/trm.mli
@@ -41,7 +41,7 @@ end
 module Arith :
   Arithmetic.S with type var := Var.t with type trm := t with type t = arith
 
-val ppx : Var.t Var.strength -> t pp
+val ppx : Var.strength -> t pp
 
 (** Construct *)