[prover][doc] MSL docs used t: type to quantify over types, but generics must be used

[wrwg]

Before monomorphization was introduced as a major performance improvement for verification times, one could use specs invariant forall T: type @ exists<R<T>>(a). This should be replaced by invariant<T> exists<R<T>>(a), but the MSL docs describe the old style.

Additionally, it is surprising that T: type seems to be still supported. Does the type type actually still works, or is it accidentally still passing the type checker as users report? If the type of types is not longer working any longer, mentioning it should be removed from the docs, and according better error message produced.