Use the monad definition in CoqOfRust.v

[clarus]

For now, in https://github.com/formal-land/coq-of-rust/blob/main/CoqOfRust/CoqOfRust.v , the definition of the monad is:

Module M.
  Parameter M : Set -> Set.
  Parameter Pure : forall {a : Set}, a -> M a.
  Parameter bind : forall {a b : Set}, M a -> (a -> M b) -> M b.

Use the definition from the file https://github.com/formal-land/coq-of-rust/blob/main/CoqOfRust/experiments/MonadExperiments.v instead. To use definitions from this file, either do a copy&paste or import these definitions from a separate file.

Many technical difficulties might appear when doing this integration.