[experiment] Use ext-lib monads

[4ever2]

Working with projects using both MetaRocq and ext-lib can be painful due to universe & notation clashes. Currently, the only difference between MetaRocq's and extlib's monad definition is cumulativity. However, cumulativity doesn't appear to be necessary for MetaRocq (I haven't yet tested this PR on all developments using MetaRocq, so it might be the case that it is needed there).

[TheoWinterhalter]

I think it is important that MetaRocq has as few dependencies as possible so it can be used in libraries, say if and when it provides adequate meta-programming facilities. I don't know what the others think.

[4ever2]

It was discussed previously #952.
The purpose of this PR was mainly to see if it was possible. I agree that we should be careful about what dependencies we use.

[mattam82]

I think we should depend on ext-lib here, no need to reinvent the wheel. I also expect we'll be using itree stuff in combination with MetaRocq in some projects, so the earlier the better. AFAIR the monad_utils was pretty much a copy-paste of ext-lib at the time, so vert probably no big compat issues switching from monad_utils to ext-lib's monads will arise. The Cumulativity is optional I think, but could be useful in some applications. ext-lib itself should have monad cumulative, it should only make it more versatile, no downsides a priori.

[4ever2]

There is a PR rocq-community/coq-ext-lib#136 adding cummulativity to ext-lib. There was interest in merging it, but there were some compatibility issues with QuickChick that haven't been solved yet.

[mattam82]

FTR, CertiCoq already depends on ext-lib as well.