proposition: Lemma getput_prepend (S : UU0) (M : nondetStateMonad S) A (m : M A) : m = get >>= (fun x => put x >> m).
proof: Proof. by rewrite -{2}(bindskipf m) -bindA getputskip 2!bindskipf. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib fail_lib