proposition: Lemma protect_put_ret {A S : UU0} {M : stateMonad S} (s : S) (a : A) : protect (put s >> Ret a) = Ret a :> M _.
proof: Proof. rewrite /protect. under eq_bind do rewrite bindA bindretf. rewrite /overwrite. under eq_bind do rewrite -bindA putput. by rewrite -bindA getputskip bindskipf. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib fail_lib