other
(in-package "ACL2")
predicate-pfunction
(defun predicate-p (term) (and (consp term) (member (car term) '(equal < integerp rationalp complex-rationalp))))
equal-of-predicates-rewritetheorem
(defthm equal-of-predicates-rewrite (implies (and (syntaxp (and (predicate-p a) (predicate-p b))) (booleanp a) (booleanp b)) (equal (equal a b) (iff a b))))