proposition: Lemma naturality : naturality [the functor of (exponential_F A \o M)] M m.
proof: Proof. move=> X Y f; apply funext => eX. set rhs := RHS. have H : Ms_R X Y (fun x y => f x = y) (m X eX) rhs. apply param => // a _ <- s1 _ <-. rewrite Actm_exponenial_FE Actm_ModelMonadStateE'. by case: (eX a) => x s2; exact: prod_R_pair_R. apply funext => s. have {}H : prod_R X Y (fun x y => f x = y) S S S_R (m X eX s) (rhs s) by exact: H. inversion H as [x y fxy s1 s2 s12 xs1 ys2]. by rewrite Actm_ModelMonadStateE -xs1 fxy s12. Qed.
imports: Param(Param) mathcomp(all_ssreflect) HB(structures) imonae_lib ihierarchy imonad_lib ifmt_lifting imonad_model