let unify_terms_ ~(recompute: bool) ?(p_preserving: bool = false)
  (subst: subst) (term1: term) (offset1: int) (term2: term) (offset2: int) : subst =

  if not recompute && p_preserving then
    UnificationPPreserving.unify_terms subst term1 offset1 term2 offset2

  else if not recompute && not p_preserving then
    Unification_Preserving.unify_terms subst term1 offset1 term2 offset2

  else if recompute && p_preserving then
    UnificationRPPreserving.unify_terms subst term1 offset1 term2 offset2

  else (* if recompute && not p_preserving then *)
    Unification_RPreserving.unify_terms subst term1 offset1 term2 offset2