Patterns for recognizing functions that return BFRs.
Function: bfr-termp
(defun bfr-termp (x bfr-terms pats) (or (member-equal x bfr-terms) (acl2::match-term-pattern x pats)))
