proposition: Lemma write_readC i j x : i != j -> aput i x >> aget j = aget j >>= (fun v => aput i x >> Ret v) :> M _.
proof: Proof. by move => ?; rewrite -aputgetC // bindmret. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib fail_lib