proposition: Lemma Actm_ModelMonadStateE' (X Y : UU0) (f : X -> Y) (eX : (exponential_F A \o M) X) a (s : S): (M # f \o eX) a s = let (x, y) := eX a 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