diff --git a/sledge/src/domain_sh.ml b/sledge/src/domain_sh.ml
index 9199a2457..cba093ba3 100644
--- a/sledge/src/domain_sh.ml
+++ b/sledge/src/domain_sh.ml
@@ -86,12 +86,12 @@ let exec_intrinsic ~skip_throw q r i es =
 let term_eq_class_has_only_vars_in fvs cong term =
   [%Trace.call fun {pf} ->
     pf "@[<v> fvs: @[%a@] @,cong: @[%a@] @,term: @[%a@]@]" Var.Set.pp fvs
-      Equality.pp cong Term.pp term]
+      Context.pp cong Term.pp term]
   ;
   let term_has_only_vars_in fvs term =
     Var.Set.is_subset (Term.fv term) ~of_:fvs
   in
-  let term_eq_class = Equality.class_of cong term in
+  let term_eq_class = Context.class_of cong term in
   List.exists ~f:(term_has_only_vars_in fvs) term_eq_class
   |>
   [%Trace.retn fun {pf} -> pf "%b"]
@@ -107,7 +107,7 @@ let garbage_collect (q : t) ~wrt =
       let new_set =
         List.fold ~init:current q.heap ~f:(fun current seg ->
             if term_eq_class_has_only_vars_in current q.cong seg.loc then
-              List.fold (Equality.class_of q.cong seg.seq) ~init:current
+              List.fold (Context.class_of q.cong seg.seq) ~init:current
                 ~f:(fun c e -> Var.Set.union c (Term.fv e))
             else current )
       in
diff --git a/sledge/src/fol.ml b/sledge/src/fol.ml
index 815af7adf..87d2e9fb3 100644
--- a/sledge/src/fol.ml
+++ b/sledge/src/fol.ml
@@ -7,4 +7,4 @@
 
 module Var = Ses.Var
 module Term = Ses.Term
-module Equality = Ses.Equality
+module Context = Ses.Equality
diff --git a/sledge/src/fol.mli b/sledge/src/fol.mli
index 815af7adf..87d2e9fb3 100644
--- a/sledge/src/fol.mli
+++ b/sledge/src/fol.mli
@@ -7,4 +7,4 @@
 
 module Var = Ses.Var
 module Term = Ses.Term
-module Equality = Ses.Equality
+module Context = Ses.Equality
diff --git a/sledge/src/sh.ml b/sledge/src/sh.ml
index 9db819adf..32085d07e 100644
--- a/sledge/src/sh.ml
+++ b/sledge/src/sh.ml
@@ -17,7 +17,7 @@ type seg = {loc: Term.t; bas: Term.t; len: Term.t; siz: Term.t; seq: Term.t}
 type starjunction =
   { us: Var.Set.t
   ; xs: Var.Set.t
-  ; cong: Equality.t
+  ; cong: Context.t
   ; pure: Term.t
   ; heap: seg list
   ; djns: disjunction list }
@@ -32,7 +32,7 @@ type t = starjunction [@@deriving compare, equal, sexp]
 let emp =
   { us= Var.Set.empty
   ; xs= Var.Set.empty
-  ; cong= Equality.true_
+  ; cong= Context.true_
   ; pure= Term.true_
   ; heap= []
   ; djns= [] }
@@ -82,7 +82,7 @@ let fold_vars_stem ?ignore_cong {us= _; xs= _; cong; pure; heap; djns= _}
   |> fun init ->
   if Option.is_some ignore_cong then init
   else
-    Equality.fold_terms ~init cong ~f:(fun init -> Term.fold_vars ~f ~init)
+    Context.fold_terms ~init cong ~f:(fun init -> Term.fold_vars ~f ~init)
 
 let fold_vars ?ignore_cong fold_vars q ~init ~f =
   fold_vars_stem ?ignore_cong ~init ~f q
@@ -137,7 +137,7 @@ let pp_seg x fs {loc; bas; len; siz; seq} =
 
 let pp_seg_norm cong fs seg =
   let x _ = None in
-  pp_seg x fs (map_seg seg ~f:(Equality.normalize cong))
+  pp_seg x fs (map_seg seg ~f:(Context.normalize cong))
 
 let pp_block x fs segs =
   let is_full_alloc segs =
@@ -179,17 +179,17 @@ let pp_heap x ?pre cong fs heap =
   in
   let compare s1 s2 =
     [%compare: Term.t * (Term.t * Q.t)]
-      ( Equality.normalize cong s1.bas
-      , bas_off (Equality.normalize cong s1.loc) )
-      ( Equality.normalize cong s2.bas
-      , bas_off (Equality.normalize cong s2.loc) )
+      ( Context.normalize cong s1.bas
+      , bas_off (Context.normalize cong s1.loc) )
+      ( Context.normalize cong s2.bas
+      , bas_off (Context.normalize cong s2.loc) )
   in
   let break s1 s2 =
     (not (Term.equal s1.bas s2.bas))
     || (not (Term.equal s1.len s2.len))
-    || not (Equality.entails_eq cong (Term.add s1.loc s1.siz) s2.loc)
+    || not (Context.entails_eq cong (Term.add s1.loc s1.siz) s2.loc)
   in
-  let heap = List.map heap ~f:(map_seg ~f:(Equality.normalize cong)) in
+  let heap = List.map heap ~f:(map_seg ~f:(Context.normalize cong)) in
   let blocks = List.group ~break (List.sort ~compare heap) in
   List.pp ?pre "@ * " (pp_block x) fs blocks
 
@@ -218,14 +218,14 @@ let rec pp_ ?var_strength vs parent_xs parent_cong fs
     if not (Var.Set.is_empty xs_d_vs) then Format.fprintf fs "@ " ) ;
   if not (Var.Set.is_empty xs_d_vs) then
     Format.fprintf fs "@<2>∃ @[%a@] .@ " (Var.Set.ppx x) xs_d_vs ;
-  let clss = Equality.diff_classes cong parent_cong in
+  let clss = Context.diff_classes cong parent_cong in
   let first = Term.Map.is_empty clss in
   if not first then Format.fprintf fs "  " ;
-  Equality.ppx_classes x fs clss ;
+  Context.ppx_classes x fs clss ;
   let pure =
     if Option.is_none var_strength then [pure]
     else
-      let pure' = Equality.normalize cong pure in
+      let pure' = Context.normalize cong pure in
       if Term.is_true pure' then [] else [pure']
   in
   List.pp
@@ -265,9 +265,9 @@ and pp_djn ?var_strength vs xs cong fs = function
 let pp_diff_eq ?(us = Var.Set.empty) ?(xs = Var.Set.empty) cong fs q =
   pp_ ~var_strength:(var_strength ~xs q) us xs cong fs q
 
-let pp fs q = pp_diff_eq Equality.true_ fs q
-let pp_djn fs d = pp_djn Var.Set.empty Var.Set.empty Equality.true_ fs d
-let pp_raw fs q = pp_ Var.Set.empty Var.Set.empty Equality.true_ fs q
+let pp fs q = pp_diff_eq Context.true_ fs q
+let pp_djn fs d = pp_djn Var.Set.empty Var.Set.empty Context.true_ fs d
+let pp_raw fs q = pp_ Var.Set.empty Var.Set.empty Context.true_ fs q
 let fv_seg seg = fold_vars_seg seg ~f:Var.Set.add ~init:Var.Set.empty
 
 let fv ?ignore_cong q =
@@ -297,13 +297,13 @@ let rec invariant q =
       Var.Set.is_subset (fv q) ~of_:us
       || fail "unbound but free: %a" Var.Set.pp (Var.Set.diff (fv q) us) ()
     ) ;
-    Equality.invariant cong ;
+    Context.invariant cong ;
     ( match djns with
     | [[]] ->
-        assert (Equality.is_true cong) ;
+        assert (Context.is_true cong) ;
         assert (Term.is_true pure) ;
         assert (List.is_empty heap)
-    | _ -> assert (not (Equality.is_false cong)) ) ;
+    | _ -> assert (not (Context.is_false cong)) ) ;
     invariant_pure pure ;
     List.iter heap ~f:invariant_seg ;
     List.iter djns ~f:(fun djn ->
@@ -320,7 +320,7 @@ let rec invariant q =
     invariant *)
 let rec apply_subst sub q =
   map q ~f_sjn:(rename sub)
-    ~f_cong:(fun r -> Equality.rename r sub)
+    ~f_cong:(fun r -> Context.rename r sub)
     ~f_trm:(Term.rename sub)
   |> check (fun q' ->
          assert (Var.Set.disjoint (fv q') (Var.Subst.domain sub)) )
@@ -437,17 +437,17 @@ let elim_exists xs q =
 
 (** conjoin an equality relation assuming vocabulary is compatible *)
 let and_cong_ cong q =
-  assert (Var.Set.is_subset (Equality.fv cong) ~of_:q.us) ;
-  let xs, cong = Equality.and_ (Var.Set.union q.us q.xs) q.cong cong in
-  if Equality.is_false cong then false_ q.us
+  assert (Var.Set.is_subset (Context.fv cong) ~of_:q.us) ;
+  let xs, cong = Context.and_ (Var.Set.union q.us q.xs) q.cong cong in
+  if Context.is_false cong then false_ q.us
   else exists_fresh xs {q with cong}
 
 let and_cong cong q =
-  [%Trace.call fun {pf} -> pf "%a@ %a" Equality.pp cong pp q]
+  [%Trace.call fun {pf} -> pf "%a@ %a" Context.pp cong pp q]
   ;
   ( match q.djns with
   | [[]] -> q
-  | _ -> and_cong_ cong (extend_us (Equality.fv cong) q) )
+  | _ -> and_cong_ cong (extend_us (Context.fv cong) q) )
   |>
   [%Trace.retn fun {pf} q ->
     pf "%a" pp q ;
@@ -460,11 +460,11 @@ let star q1 q2 =
   | {djns= [[]]; _}, _ | _, {djns= [[]]; _} ->
       false_ (Var.Set.union q1.us q2.us)
   | {us= _; xs= _; cong; pure; heap= []; djns= []}, _
-    when Equality.is_true cong && Term.is_true pure ->
+    when Context.is_true cong && Term.is_true pure ->
       let us = Var.Set.union q1.us q2.us in
       if us == q2.us then q2 else {q2 with us}
   | _, {us= _; xs= _; cong; pure; heap= []; djns= []}
-    when Equality.is_true cong && Term.is_true pure ->
+    when Context.is_true cong && Term.is_true pure ->
       let us = Var.Set.union q1.us q2.us in
       if us == q1.us then q1 else {q1 with us}
   | _ ->
@@ -475,9 +475,9 @@ let star q1 q2 =
       let {us= us2; xs= xs2; cong= c2; pure= p2; heap= h2; djns= d2} = q2 in
       assert (Var.Set.equal us (Var.Set.union us1 us2)) ;
       let xs, cong =
-        Equality.and_ (Var.Set.union us (Var.Set.union xs1 xs2)) c1 c2
+        Context.and_ (Var.Set.union us (Var.Set.union xs1 xs2)) c1 c2
       in
-      if Equality.is_false cong then false_ us
+      if Context.is_false cong then false_ us
       else
         exists_fresh xs
           { us
@@ -514,7 +514,7 @@ let or_ q1 q2 =
   | _ ->
       { us= Var.Set.union q1.us q2.us
       ; xs= Var.Set.empty
-      ; cong= Equality.true_
+      ; cong= Context.true_
       ; pure= Term.true_
       ; heap= []
       ; djns= [[q1; q2]] } )
@@ -534,8 +534,8 @@ let pure (e : Term.t) =
   ;
   List.fold (Term.disjuncts e) ~init:(false_ Var.Set.empty) ~f:(fun q b ->
       let us = Term.fv b in
-      let xs, cong = Equality.(and_term us b true_) in
-      if Equality.is_false cong then false_ us
+      let xs, cong = Context.(and_term us b true_) in
+      if Context.is_false cong then false_ us
       else or_ q (exists_fresh xs {emp with us; cong; pure= b}) )
   |>
   [%Trace.retn fun {pf} q ->
@@ -545,9 +545,9 @@ let pure (e : Term.t) =
 let and_ e q = star (pure e) q
 
 let and_subst subst q =
-  [%Trace.call fun {pf} -> pf "%a@ %a" Equality.Subst.pp subst pp q]
+  [%Trace.call fun {pf} -> pf "%a@ %a" Context.Subst.pp subst pp q]
   ;
-  Equality.Subst.fold
+  Context.Subst.fold
     ~f:(fun ~key ~data -> and_ (Term.eq key data))
     subst ~init:q
   |>
@@ -595,9 +595,9 @@ let is_emp = function
 let is_false = function
   | {djns= [[]]; _} -> true
   | {cong; pure; heap; _} ->
-      Term.is_false (Equality.normalize cong pure)
+      Term.is_false (Context.normalize cong pure)
       || List.exists heap ~f:(fun seg ->
-             Equality.entails_eq cong seg.loc Term.zero )
+             Context.entails_eq cong seg.loc Term.zero )
 
 let rec pure_approx ({us; xs; cong; pure; heap= _; djns} as q) =
   let heap = emp.heap in
@@ -647,12 +647,12 @@ let dnf q =
 (** Simplify *)
 
 let rec norm_ s q =
-  [%Trace.call fun {pf} -> pf "@[%a@]@ %a" Equality.Subst.pp s pp_raw q]
+  [%Trace.call fun {pf} -> pf "@[%a@]@ %a" Context.Subst.pp s pp_raw q]
   ;
   let q =
-    map q ~f_sjn:(norm_ s) ~f_cong:Fn.id ~f_trm:(Equality.Subst.subst s)
+    map q ~f_sjn:(norm_ s) ~f_cong:Fn.id ~f_trm:(Context.Subst.subst s)
   in
-  let xs, cong = Equality.apply_subst (Var.Set.union q.us q.xs) s q.cong in
+  let xs, cong = Context.apply_subst (Var.Set.union q.us q.xs) s q.cong in
   exists_fresh xs {q with cong}
   |>
   [%Trace.retn fun {pf} q' ->
@@ -660,9 +660,9 @@ let rec norm_ s q =
     invariant q']
 
 let norm s q =
-  [%Trace.call fun {pf} -> pf "@[%a@]@ %a" Equality.Subst.pp s pp_raw q]
+  [%Trace.call fun {pf} -> pf "@[%a@]@ %a" Context.Subst.pp s pp_raw q]
   ;
-  (if Equality.Subst.is_empty s then q else norm_ s q)
+  (if Context.Subst.is_empty s then q else norm_ s q)
   |>
   [%Trace.retn fun {pf} q' ->
     pf "%a" pp_raw q' ;
@@ -695,7 +695,7 @@ let rec freshen_nested_xs q =
 
 let rec propagate_equality_ ancestor_vs ancestor_cong q =
   [%Trace.call fun {pf} ->
-    pf "(%a)@ %a" Equality.pp_classes ancestor_cong pp q]
+    pf "(%a)@ %a" Context.pp_classes ancestor_cong pp q]
   ;
   (* extend vocabulary with variables in scope above *)
   let ancestor_vs = Var.Set.union ancestor_vs (Var.Set.union q.us q.xs) in
@@ -713,9 +713,9 @@ let rec propagate_equality_ ancestor_vs ancestor_cong q =
                let dj = propagate_equality_ ancestor_vs ancestor_cong dj in
                (dj.cong, dj) )
          in
-         let new_xs, djn_cong = Equality.orN ancestor_vs dj_congs in
+         let new_xs, djn_cong = Context.orN ancestor_vs dj_congs in
          (* hoist xs appearing in disjunction's equality relation *)
-         let djn_xs = Var.Set.diff (Equality.fv djn_cong) q'.us in
+         let djn_xs = Var.Set.diff (Context.fv djn_cong) q'.us in
          let djn = List.map ~f:(elim_exists djn_xs) djn in
          let cong_djn = and_cong_ djn_cong (orN djn) in
          assert (is_false cong_djn || Var.Set.is_subset new_xs ~of_:djn_xs) ;
@@ -727,7 +727,7 @@ let rec propagate_equality_ ancestor_vs ancestor_cong q =
 
 let propagate_equality ancestor_vs ancestor_cong q =
   [%Trace.call fun {pf} ->
-    pf "(%a)@ %a" Equality.pp_classes ancestor_cong pp q]
+    pf "(%a)@ %a" Context.pp_classes ancestor_cong pp q]
   ;
   propagate_equality_ ancestor_vs ancestor_cong q
   |>
@@ -745,14 +745,14 @@ let remove_absent_xs ks q =
   if Var.Set.is_empty ks then q
   else
     let xs = Var.Set.diff q.xs ks in
-    let cong = Equality.elim ks q.cong in
+    let cong = Context.elim ks q.cong in
     let djns =
       let rec trim_ks ks djns =
         List.map djns ~f:(fun djn ->
             List.map djn ~f:(fun sjn ->
                 { sjn with
                   us= Var.Set.diff sjn.us ks
-                ; cong= Equality.elim ks sjn.cong
+                ; cong= Context.elim ks sjn.cong
                 ; djns= trim_ks ks sjn.djns } ) )
       in
       trim_ks ks q.djns
@@ -773,10 +773,10 @@ let rec simplify_ us rev_xss q =
          ))
   in
   (* try to solve equations in cong for variables in xss *)
-  let subst = Equality.solve_for_vars (us :: List.rev rev_xss) q.cong in
+  let subst = Context.solve_for_vars (us :: List.rev rev_xss) q.cong in
   (* simplification can reveal inconsistency *)
   ( if is_false q then false_ q.us
-  else if Equality.Subst.is_empty subst then q
+  else if Context.Subst.is_empty subst then q
   else
     (* normalize wrt solutions *)
     let q = norm subst q in
@@ -786,20 +786,20 @@ let rec simplify_ us rev_xss q =
         (Var.Set.union_list rev_xss)
         (fv ~ignore_cong:() (elim_exists q.xs q))
     in
-    let keep, removed, _ = Equality.Subst.partition_valid removed subst in
+    let keep, removed, _ = Context.Subst.partition_valid removed subst in
     let q = and_subst keep q in
     (* remove the eliminated variables from xs and subformulas' us *)
     remove_absent_xs removed q )
   |>
   [%Trace.retn fun {pf} q' ->
-    pf "%a@ %a" Equality.Subst.pp subst pp_raw q' ;
+    pf "%a@ %a" Context.Subst.pp subst pp_raw q' ;
     invariant q']
 
 let simplify q =
   [%Trace.call fun {pf} -> pf "%a" pp_raw q]
   ;
   let q = freshen_nested_xs q in
-  let q = propagate_equality Var.Set.empty Equality.true_ q in
+  let q = propagate_equality Var.Set.empty Context.true_ q in
   let q = simplify_ q.us [] q in
   q
   |>
diff --git a/sledge/src/sh.mli b/sledge/src/sh.mli
index 8595ec8d0..a3df73030 100644
--- a/sledge/src/sh.mli
+++ b/sledge/src/sh.mli
@@ -17,7 +17,7 @@ type seg = {loc: Term.t; bas: Term.t; len: Term.t; siz: Term.t; seq: Term.t}
 type starjunction = private
   { us: Var.Set.t  (** vocabulary / variable context of formula *)
   ; xs: Var.Set.t  (** existentially-bound variables *)
-  ; cong: Equality.t  (** congruence induced by rest of formula *)
+  ; cong: Context.t  (** congruence induced by rest of formula *)
   ; pure: Term.t  (** pure boolean constraints *)
   ; heap: seg list  (** star-conjunction of segment atomic formulas *)
   ; djns: disjunction list  (** star-conjunction of disjunctions *) }
@@ -26,11 +26,11 @@ and disjunction = starjunction list
 
 type t = starjunction [@@deriving compare, equal, sexp]
 
-val pp_seg_norm : Equality.t -> seg pp
+val pp_seg_norm : Context.t -> seg pp
 val pp_us : ?pre:('a, 'a) fmt -> ?vs:Var.Set.t -> unit -> Var.Set.t pp
 val pp : t pp
 val pp_raw : t pp
-val pp_diff_eq : ?us:Var.Set.t -> ?xs:Var.Set.t -> Equality.t -> t pp
+val pp_diff_eq : ?us:Var.Set.t -> ?xs:Var.Set.t -> Context.t -> t pp
 val pp_djn : disjunction pp
 val simplify : t -> t
 
@@ -61,11 +61,11 @@ val pure : Term.t -> t
 val and_ : Term.t -> t -> t
 (** Conjoin a boolean constraint to a formula. *)
 
-val and_cong : Equality.t -> t -> t
+val and_cong : Context.t -> t -> t
 (** Conjoin constraints of a congruence to a formula, extending to a common
     vocabulary, and avoiding capturing existentials. *)
 
-val and_subst : Equality.Subst.t -> t -> t
+val and_subst : Context.Subst.t -> t -> t
 (** Conjoin constraints of a solution substitution to a formula, extending
     to a common vocabulary, and avoiding capturing existentials. *)
 
@@ -85,7 +85,7 @@ val rem_seg : seg -> t -> t
 val filter_heap : f:(seg -> bool) -> t -> t
 (** [filter_heap q f] Remove all segments in [q] for which [f] returns false *)
 
-val norm : Equality.Subst.t -> t -> t
+val norm : Context.Subst.t -> t -> t
 (** [norm s q] is [q] where subterms have been normalized with a
     substitution. *)
 
diff --git a/sledge/src/solver.ml b/sledge/src/solver.ml
index fd7fb2ba9..5a137502f 100644
--- a/sledge/src/solver.ml
+++ b/sledge/src/solver.ml
@@ -158,9 +158,9 @@ let excise_exists goal =
         Var.Set.diff goal.xs
           (Sh.fv ~ignore_cong:() (Sh.with_pure Term.true_ goal.sub))
       in
-      Equality.solve_for_vars [Var.Set.empty; goal.us; xs] goal.sub.cong
+      Context.solve_for_vars [Var.Set.empty; goal.us; xs] goal.sub.cong
     in
-    if Equality.Subst.is_empty solutions_for_xs then goal
+    if Context.Subst.is_empty solutions_for_xs then goal
     else
       let removed =
         Var.Set.diff goal.xs
@@ -169,13 +169,13 @@ let excise_exists goal =
       if Var.Set.is_empty removed then goal
       else
         let _, removed, witnesses =
-          Equality.Subst.partition_valid removed solutions_for_xs
+          Context.Subst.partition_valid removed solutions_for_xs
         in
-        if Equality.Subst.is_empty witnesses then goal
+        if Context.Subst.is_empty witnesses then goal
         else (
           excise (fun {pf} ->
               pf "@[<2>excise_exists @[%a%a@]@]" Var.Set.pp_xs removed
-                Equality.Subst.pp witnesses ) ;
+                Context.Subst.pp witnesses ) ;
           let us = Var.Set.union goal.us removed in
           let xs = Var.Set.diff goal.xs removed in
           let min = Sh.and_subst witnesses goal.min in
@@ -183,7 +183,7 @@ let excise_exists goal =
 
 let excise_pure ({min; sub} as goal) =
   trace (fun {pf} -> pf "@[<2>excise_pure@ %a@]" pp goal) ;
-  let pure' = Equality.normalize min.cong sub.pure in
+  let pure' = Context.normalize min.cong sub.pure in
   if Term.is_false pure' then None
   else Some (goal |> with_ ~sub:(Sh.with_pure pure' sub))
 
@@ -562,10 +562,10 @@ let excise_seg ({sub} as goal) msg ssg =
         (Sh.pp_seg_norm sub.cong) ssg ) ;
   let {Sh.loc= k; bas= b; len= m; siz= o} = msg in
   let {Sh.loc= l; bas= b'; len= m'; siz= n} = ssg in
-  let* k_l = Equality.difference sub.cong k l in
+  let* k_l = Context.difference sub.cong k l in
   if
-    (not (Equality.entails_eq sub.cong b b'))
-    || not (Equality.entails_eq sub.cong m m')
+    (not (Context.entails_eq sub.cong b b'))
+    || not (Context.entails_eq sub.cong m m')
   then
     Some
       ( goal
@@ -578,11 +578,11 @@ let excise_seg ({sub} as goal) msg ssg =
     | Neg -> (
         let ko = Term.add k o in
         let ln = Term.add l n in
-        let* ko_ln = Equality.difference sub.cong ko ln in
+        let* ko_ln = Context.difference sub.cong ko ln in
         match Int.sign (Z.sign ko_ln) with
         (* k+o-(l+n) < 0 so k+o < l+n *)
         | Neg -> (
-            let* l_ko = Equality.difference sub.cong l ko in
+            let* l_ko = Context.difference sub.cong l ko in
             match Int.sign (Z.sign l_ko) with
             (* l-(k+o) < 0     [k;   o)
              * so l < k+o    ⊢    [l;  n) *)
@@ -600,7 +600,7 @@ let excise_seg ({sub} as goal) msg ssg =
         )
     (* k-l = 0 so k = l *)
     | Zero -> (
-        let* o_n = Equality.difference sub.cong o n in
+        let* o_n = Context.difference sub.cong o n in
         match Int.sign (Z.sign o_n) with
         (* o-n < 0      [k; o)
          * so o < n   ⊢ [l;   n) *)
@@ -615,7 +615,7 @@ let excise_seg ({sub} as goal) msg ssg =
     | Pos -> (
         let ko = Term.add k o in
         let ln = Term.add l n in
-        let* ko_ln = Equality.difference sub.cong ko ln in
+        let* ko_ln = Context.difference sub.cong ko ln in
         match Int.sign (Z.sign ko_ln) with
         (* k+o-(l+n) < 0        [k; o)
          * so k+o < l+n    ⊢ [l;      n) *)
@@ -625,7 +625,7 @@ let excise_seg ({sub} as goal) msg ssg =
         | Zero -> Some (excise_seg_min_suffix goal msg ssg k_l)
         (* k+o-(l+n) > 0 so k+o > l+n *)
         | Pos -> (
-            let* k_ln = Equality.difference sub.cong k ln in
+            let* k_ln = Context.difference sub.cong k ln in
             match Int.sign (Z.sign k_ln) with
             (* k-(l+n) < 0        [k;  o)
              * so k < l+n    ⊢ [l;   n) *)