let remove_context_var_renamings (subst: subst) : subst =
  let subst =
    normalize_var_renamings subst
  in
  List.find_all
    (fun binding ->
       (* keep all clause literal variables -
          this are used to actually instantiate the remainder literals
          (Selection_assert, Selection_split, Context_unifier_check) *)
       binding.sb_var.sv_offset == input_literal_offset
       ||
       (
         (* keep if ... *)
         List.exists
           (fun binding' ->
              (* ... another variable *)
              binding' != binding
              &&
              (* ... is bound to a context term *)
              binding'.sb_term.st_offset == binding.sb_var.sv_offset
              &&
              (* ... containing this variable *)
              Term.term_contains_var binding'.sb_term.st_term binding.sb_var.sv_var
           )
           subst
       )
    )
    subst