Removing a requirement in toi_promote which is confusing and unnece… (#4507)

This PR removes a requirement in `toi_promote` which is confusing and unnecessary.

Author: eernstg

resources/type-system/flow-analysis.md

@@ -471,9 +471,9 @@ Definitions:
     _The types in `p1` are known as the types of interest._
   - Let `p2` be the set `p1 \ { provisionalType }` _(where `\` denotes set
     difference)_.
-  - If the `written` type is in `p2`, and `written <: provisionalType`, then
-    `newPromotionChain` is `[...promotionChain, written]`. _Writing a value
-    whose static type is a type of interest promotes to that type._
+  - If the `written` type is in `p2` then `newPromotionChain` is
+    `[...promotionChain, written]`. _Writing a value whose static type is a
+    type of interest promotes to that type._
     - _By precondition, `written <: declared` and `written <: T` for all types
       in `promotionChain`. Therefore, `newPromotionChain` satisfies the
       definition of a promotion chain, and is valid for declared type