Improved type-set reasoning for a few built-in functions.

Quoting :doc note-7-0:

  [Type-set] reasoning has been improved for a few built-in functions,
  including first-n-ac, [substitute], [nthcdr], and [subseq], and
  thus for some functions whose computed type depends on one of
  these: for example, [take] and therefore, also [butlast] and
  [subseq-list], are now known to return [true-listp] results. Thanks
  to Jared Davis for a request that led us to these changes. In
  particular, the definitions of first-n-ac and substitute-ac have
  been modified to call [revappend] instead of [reverse], and the
  following :[type-prescription] rules have been added to source file
  axioms.lisp (and can be seen using :[pe]).

    * true-listp-first-n-ac-type-prescription
    * stringp-substitute-type-prescription
    * true-listp-substitute-type-prescription
    * true-listp-nthcdr-type-prescription
    * stringp-subseq-type-prescription
    * true-listp-subseq-type-prescription

  Technical note on the above change: in some cases, the built-in
  :[type-prescription] rule has been changed, essentially for the
  better, but new rules have also been added. Consider for example
  the function, [substitute]. This function calls substitute-ac,
  which in turn now calls [revappend] instead of [reverse], which
  allows ACL2 to deduce a :type-prescription rule saying that
  substitute returns a string or a true-list. However, new
  :type-prescription rules stringp-substitute-type-prescription and
  true-listp-substitute-type-prescription allow the stronger
  conclusion that substitute returns a string or true-list,
  respectively depending on whether [type-set] reasoning can deduce
  that the given sequence is or is not a string. The deduced
  :type-prescription rule can still be of some use in cases that
  type-set reasoning cannot establish whether or not the input
  sequence is a string.