acceptable-rewrite-rule-p

(defun acceptable-rewrite-rule-p1
  (name lst ens wrld)
  (cond ((null lst) t)
    (t (mv-let (msg eqv lhs0 lhs rhs ttree)
        (interpret-term-as-rewrite-rule nil
          name
          (caar lst)
          (cdar lst)
          nil
          ens
          wrld)
        (declare (ignore eqv lhs0 lhs rhs ttree))
        (and (null msg)
          (acceptable-rewrite-rule-p1 name (cdr lst) ens wrld))))))

(defun acceptable-rewrite-rule-p
  (term ens wrld)
  (acceptable-rewrite-rule-p1 :some-proposed-rewrite-rule (unprettyify (remove-guard-holders term wrld))
    ens
    wrld))