Updates to generics design details, part 2 (#3253)

Continued from part 1: #3231. Second step updating
`docs/design/generics/details.md`. There remains some work to
incorporate proposal #2200.

- The biggest changes are incorporating much of the text of proposals:
  - #2173
  - #2687
- It incorporates changes from proposals:
  - #989
  - #1178
  - #2138
  - #2200
  - #2360
  - #2964
  - #3162
- It also updates the text to reflect the latest thinking from leads
issues:
  - #996
  - #2153 -- most notably deleting the section on `TypeId`.
- Update to rule for prioritization blocks with mixed type structures
from [discussion on
2023-07-18](https://docs.google.com/document/d/1gnJBTfY81fZYvI_QXjwKk1uQHYBNHGqRLI2BS_cYYNQ/edit?resourcekey=0-ql1Q1WvTcDvhycf8LbA9DQ#heading=h.7jxges9ojgy3)
- Adds reference links to proposals, issues, and discussions relevant to
the text.
- Also tries to use more precise language when talking about
implementations, to avoid confusing `impl` declaration and definitions
with the `impls` operator used in `where` clauses, an issue brought up
in
  - #2495 
  - #2483

---------

Co-authored-by: Richard Smith <[email protected]>

docs/design/generics/README.md

@@ -17,8 +17,11 @@ feature of Carbon:
 -   [Terminology](terminology.md) - A glossary establishing common terminology
     for describing the design
 -   [Detailed design](details.md) - In-depth description
+    -   [Appendix: Coherence](appendix-coherence.md) - Describes the rationale
+        for Carbon's choice to have coherent generics, and the alternatives.
+    -   [Appendix: Rewrite constraints](appendix-rewrite-constraints.md) -
+        Describes the detailed rules governing rewrite constraints, and why
+        resolving them terminates.
     -   [Appendix: Witness tables](appendix-witness.md) - Describes an
         implementation strategy for checked generics, and Carbon's rationale for
         only using it for dynamic dispatch.
-    -   [Appendix: Coherence](appendix-coherence.md) - Describes the rationale
-        for Carbon's choice to have coherent generics, and the alternatives.