		Search-engine friendly clone of the ACL2 documentation.

Renamings

Renaming-pair-equality

Theorem about pair equality in renamings.

Two pairs in a renaming are equal if and only if their cars or their cdrs are equal. This is because there cannot be two distinct pairs with the same car or cdr.

Definitions and Theorems

Theorem: renaming-pair-equality

(defthm renaming-pair-equality
  (implies (and (member-equal pair1 (renaming->list ren))
                (member-equal pair2 (renaming->list ren)))
           (equal (equal pair1 pair2)
                  (or (equal (car pair1) (car pair2))
                      (equal (cdr pair1) (cdr pair2))))))