proposition: Lemma natural_psi' (n : E ~> M) : naturality [the functor of E \o M] M (psi' n).
proof: Proof. move=> A B h; rewrite /psi'. rewrite -/(Join \o n (M A)) [LHS]compA natural. by rewrite -compA (natural n). Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib ifail_lib istate_lib