let is_term_generalization ?(p_preserving: bool = false)
    (general: term) (instance: term) : bool =
  try
    ignore (
      match_terms ~recompute:false ~p_preserving:p_preserving
        general 0 instance 1 : subst
    );
    true
  with
    | UNIFICATION_FAIL ->
        false