let are_terms_unifiable ?(p_preserving: bool = false)
    (x: term) (y: term) : bool =
  try
    ignore (
      unify_terms ~recompute:false ~p_preserving:p_preserving
        x 0 y 1 : subst
    );
    true
  with
    | UNIFICATION_FAIL  ->
        false