Update observe design doc to reflect proposal #7545 (#7617)

This adds the new restrictions introduced for `observe` declarations
inside `interface` definitions to the docs.

---------

Co-authored-by: Christopher Di Bella <cjdb.ns@gmail.com>

docs/design/generics/details.md

@@ -3261,6 +3261,34 @@ the expression `G.E.N.E.N` is one equality away from `G.N.E.N` and so it is
 allowed. This is true even though `G.N.E.N` isn't the type expression
 immediately prior to `G.E.N.E.N`.
 
+An `observe` declaration inside an `interface` definition may only refer to
+names dependent on:
+
+-   `.Self`,
+-   generic parameters, and
+-   associated constants that are part of the enclosing `interface`.
+
+Equivalence chains may include at most one unrelated value.
+`observe .. == .. impls` declarations may include unrelated values that
+immediately satisfy the `impls` constraint.
+
+The `observe` declaration in the example below is allowed because `X.T` and
+`Y.T` are equivalent to `i32`, and `i32` directly satisfies the `Core.AddWith`
+constraint.
+
+```carbon
+interface A {
+    let T: type;
+}
+
+interface B {
+    let X: A where .T == i32;
+    let Y: A where .T == i32;
+
+    observe .X.T == i32 == .Y.T impls AddWith;
+}
+```
+
 After an `observe` declaration, all of the listed type expressions are
 considered equal to each other using a single `where` equality. In this example,
 the `observe` declaration in the `Transitive` interface definition provides the