Identical defthm events are now redundant.

  A [defthm] or [defaxiom] event is now redundant when there is already
  a syntactically identical event in the logical [world], even if the
  rules suggested by the two [events] differ. See [redundant-events].
  Thanks to Jared Davis and Sol Swords for sending the following
  example, which illustrates the change. Previously, the final event
  was not redundant, and hence failed. Now, it is redundant, even
  though the :typed-term suggested by the new [type-prescription]
  rule is (booleanp (foop x)) where the existing rule's :typed-term
  is (foop x).

    (defund foop (x) (consp x))

    (defthm booleanp-of-foop
      (booleanp (foop x))
      :rule-classes :type-prescription)

    (in-theory (disable booleanp-compound-recognizer))

    (defthm booleanp-of-foop
      (booleanp (foop x))
      :rule-classes :type-prescription)