Replaced a couple of congruence rule errors with warnings.  Updated :doc coerce about string construction.

Quoting :doc note-7-0:

  We replaced an error with a warning for cases where a classic
  [congruence] rule is unnecessary. Thanks to Jared Davis for sending
  us an example suggesting the need for a change. (See ACL2 source
  function chk-acceptable-congruence-rule for his example and more
  explanation.)

Also, updated :doc coerce with a logical note about viewing coerce as
the constructor for strings.