proposition: Lemma natural_phi' (op : E.-operation M) : naturality E M (phi' op).
proof: Proof. move=> A B h; rewrite /phi'. rewrite compA. rewrite (natural op). rewrite -compA. rewrite -[in RHS]compA. congr (_ \o _). rewrite /=. rewrite -2!(@functor_o E). by rewrite (natural ret) FIdE. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib ifail_lib istate_lib