diff --git a/sledge/nonstdlib/set.ml b/sledge/nonstdlib/set.ml
index 9fc8979cd..544408c8d 100644
--- a/sledge/nonstdlib/set.ml
+++ b/sledge/nonstdlib/set.ml
@@ -40,7 +40,7 @@ end) : S with type elt = Elt.t = struct
   let union_list ss = List.fold ~f:union ss empty
   let is_empty = S.is_empty
   let cardinal = S.cardinal
-  let mem s x = S.mem x s
+  let mem = S.mem
   let subset s ~of_:t = S.subset s t
   let disjoint = S.disjoint
   let max_elt = S.max_elt_opt
diff --git a/sledge/nonstdlib/set_intf.ml b/sledge/nonstdlib/set_intf.ml
index 3cfd2fc23..6329df90c 100644
--- a/sledge/nonstdlib/set_intf.ml
+++ b/sledge/nonstdlib/set_intf.ml
@@ -36,7 +36,7 @@ module type S = sig
 
   val is_empty : t -> bool
   val cardinal : t -> int
-  val mem : t -> elt -> bool
+  val mem : elt -> t -> bool
   val subset : t -> of_:t -> bool
   val disjoint : t -> t -> bool
   val max_elt : t -> elt option
diff --git a/sledge/src/arithmetic.ml b/sledge/src/arithmetic.ml
index 9a6a2988f..351db6bb7 100644
--- a/sledge/src/arithmetic.ml
+++ b/sledge/src/arithmetic.ml
@@ -300,7 +300,8 @@ struct
 
     (* solve *)
 
-    let exists_fv_in vs poly = Iter.exists ~f:(Var.Set.mem vs) (vars poly)
+    let exists_fv_in vs poly =
+      Iter.exists ~f:(fun v -> Var.Set.mem v vs) (vars poly)
 
     (** [solve_for_mono r c m p] solves [0 = r + (c×m) + p] as [m = q]
         ([Some (m, q)]) such that [r + (c×m) + p = m - q] *)
diff --git a/sledge/src/llair/llair.ml b/sledge/src/llair/llair.ml
index 2e0331b3b..7be1ade09 100644
--- a/sledge/src/llair/llair.ml
+++ b/sledge/src/llair/llair.ml
@@ -542,7 +542,7 @@ let set_derived_metadata functions =
       else
         let ancestors = Block_label.Set.add src ancestors in
         let jump jmp =
-          if Block_label.Set.mem ancestors jmp.dst then
+          if Block_label.Set.mem jmp.dst ancestors then
             jmp.retreating <- true
           else visit ancestors func jmp.dst
         in
@@ -557,7 +557,7 @@ let set_derived_metadata functions =
                 Func.find (Reg.name reg) functions
               with
             | Some func ->
-                if Block_label.Set.mem ancestors func.entry then
+                if Block_label.Set.mem func.entry ancestors then
                   call.recursive <- true
                 else visit ancestors func func.entry
             | None ->
diff --git a/sledge/src/ses/equality.ml b/sledge/src/ses/equality.ml
index 4c3d6bce2..48da4aa0a 100644
--- a/sledge/src/ses/equality.ml
+++ b/sledge/src/ses/equality.ml
@@ -139,7 +139,7 @@ end = struct
       [ys ⊆ xs]. *)
   let is_valid_eq xs e f =
     let is_var_in xs e =
-      Option.exists ~f:(Var.Set.mem xs) (Var.of_term e)
+      Option.exists ~f:(fun x -> Var.Set.mem x xs) (Var.of_term e)
     in
     ( is_var_in xs e
     || is_var_in xs f
@@ -280,14 +280,14 @@ and solve_ ?f d e s =
       | Some m -> solve_ ?f n m s )
       >>= solve_ ?f a b
   | Some ((Var _ as v), (Ap3 (Extract, _, _, l) as e)) ->
-      if not (Var.Set.mem (Term.fv e) (Var.of_ v)) then
+      if not (Var.Set.mem (Var.of_ v) (Term.fv e)) then
         (* v = α[o,l) ==> v ↦ α[o,l) when v ∉ fv(α[o,l)) *)
         compose1 ?f ~var:v ~rep:e s
       else
         (* v = α[o,l) ==> α[o,l) ↦ ⟨l,v⟩ when v ∈ fv(α[o,l)) *)
         compose1 ?f ~var:e ~rep:(Term.sized ~siz:l ~seq:v) s
   | Some ((Var _ as v), (ApN (Concat, a0V) as c)) ->
-      if not (Var.Set.mem (Term.fv c) (Var.of_ v)) then
+      if not (Var.Set.mem (Var.of_ v) (Term.fv c)) then
         (* v = α₀^…^αᵥ ==> v ↦ α₀^…^αᵥ when v ∉ fv(α₀^…^αᵥ) *)
         compose1 ?f ~var:v ~rep:c s
       else
diff --git a/sledge/src/ses/term.ml b/sledge/src/ses/term.ml
index 6b03b7d1e..625cae597 100644
--- a/sledge/src/ses/term.ml
+++ b/sledge/src/ses/term.ml
@@ -1170,7 +1170,8 @@ let rec height = function
 (** Solve *)
 
 let exists_fv_in vs qset =
-  Qset.exists qset ~f:(fun e _ -> exists_vars e ~f:(Var.Set.mem vs))
+  Qset.exists qset ~f:(fun e _ ->
+      exists_vars e ~f:(fun v -> Var.Set.mem v vs) )
 
 (* solve [0 = rejected_sum + (coeff × mono) + sum] *)
 let solve_for_mono rejected_sum coeff mono sum =
diff --git a/sledge/src/ses/var0.ml b/sledge/src/ses/var0.ml
index 1056e3211..781417e85 100644
--- a/sledge/src/ses/var0.ml
+++ b/sledge/src/ses/var0.ml
@@ -69,7 +69,7 @@ module Make (T : REPR) = struct
         Map.fold s (Set.empty, Set.empty)
           ~f:(fun ~key ~data (domain, range) ->
             (* substs are injective *)
-            assert (not (Set.mem range data)) ;
+            assert (not (Set.mem data range)) ;
             (Set.add key domain, Set.add data range) )
       in
       assert (Set.disjoint domain range)
@@ -105,13 +105,13 @@ module Make (T : REPR) = struct
     let restrict sub vs =
       Map.fold sub {sub; dom= Set.empty; rng= Set.empty}
         ~f:(fun ~key ~data z ->
-          if Set.mem vs key then
+          if Set.mem key vs then
             {z with dom= Set.add key z.dom; rng= Set.add data z.rng}
           else (
             assert (
               (* all substs are injective, so the current mapping is the
                  only one that can cause [data] to be in [rng] *)
-              (not (Set.mem (range (Map.remove key sub)) data))
+              (not (Set.mem data (range (Map.remove key sub))))
               || violates invariant sub ) ;
             {z with sub= Map.remove key z.sub} ) )
       |> check (fun {sub; dom; rng} ->
diff --git a/sledge/src/sh.ml b/sledge/src/sh.ml
index 812965d31..ac30ede56 100644
--- a/sledge/src/sh.ml
+++ b/sledge/src/sh.ml
@@ -97,7 +97,7 @@ let rec var_strength_ xs m q =
   let xs = Var.Set.union xs q.xs in
   let m_stem =
     fold_vars_stem ~ignore_ctx:() q m ~f:(fun var m ->
-        if not (Var.Set.mem xs var) then
+        if not (Var.Set.mem var xs) then
           Var.Map.add ~key:var ~data:`Universal m
         else add var m )
   in