update MSL doc

Author: rahxephon89

apps/nextra/pages/en/build/smart-contracts/prover/spec-lang.mdx

@@ -136,12 +136,6 @@ exists <binding>, ..., <binding> [ where <exp> ] : <exp>
 - The optional constraint `where <exp>` allows to restrict the quantified range. `forall x: T where p: q`
   is equivalent to `forall x: T : p ==> q` and `exists x: T where p: q` is equivalent to `exists x: T : p && q`.
 
-Notice that it is possible to quantify over types. For example:
-
-```move
-forall t: type, addr: address where exists<R<t>>(addr): exists<T<t>>(addr)
-```
-
 ## Choice operator
 
 The choice operator allows selecting a value that satisfies a predicate:
@@ -658,20 +652,6 @@ module 0x42::m {
 }
 ```
 
-If this is not wanted, and the `aborts_with` should be independent of `aborts_if`, one can use the
-property `[check]`:
-
-```move
-module 0x42::m {
-  spec get_one_off {
-    aborts_if !exists<Counter>(addr) with 3;
-    aborts_if global<Counter>(addr) == 0 with EXECUTION_FAILURE;
-
-    aborts_with [check] 3, EXECUTION_FAILURE;
-  }
-}
-```
-
 ## Requires condition
 
 The `requires` condition is a spec block member that postulates a pre-condition for a function. The
@@ -857,6 +837,14 @@ module 0x42::m {
 }
 ```
 
+Notice that type parameters are supported in global invariants. For example:
+
+```move
+module addr::M {
+    invariant<Y> forall addr: address where exists<R<Y>>(addr): exists<T<Y>>(addr);
+}
+```
+
 #### Disabling invariants
 
 There are times when a global invariant holds almost everywhere, except for a brief interval inside a function. In current Move code, this often occurs when something (e.g. an account) is being set up and