proposition: Lemma Actm_ModelMonadStateE (X Y : UU0) (f : X -> Y) (eX : A -> S -> (X * S)) (s : S) (mX : (A -> Ms X) -> Ms X) : (M # f \o mX) eX s = (let (x, y) := mX eX s in (f x, y)).
proof: Proof. by []. Qed.
imports: Param(Param) mathcomp(all_ssreflect) HB(structures) imonae_lib ihierarchy imonad_lib ifmt_lifting imonad_model