with-arith-help

(defun allow-arith-help-fn
  (world)
  (cond ((check-for-arith1-rulesets world) (cond ((check-for-arith5-rulesets world) '(value-triple :redundant-allow-arith-help))
        (t *allow-arith5-help-form*)))
    ((check-for-arith5-rulesets world) *allow-arith5-help-form*)
    (t `(local (progn ,*ALLOW-ARITH1-HELP-FORM*
          ,*ALLOW-ARITH5-HELP-FORM*
          (include-book "arithmetic/top-with-meta" :dir :system)
          (in-theory (current-theory 'before-including-arithmetic-1)))))))