proposition: Lemma phiK (op : E.-aoperation M) : psi (phi op) = op.
proof: Proof. apply/aoperation_ext => A. rewrite /=. rewrite psiE phiE; apply funext => m /=. rewrite -(compE (op _)) joinE. rewrite (algebraic op). rewrite -(compE (E # _)) -functor_o. rewrite -(compE (op _)). set x := _^~ id. rewrite (_ : x = Join); last first. apply: funext => mma. by rewrite /x bindE functor_id . by rewrite joinretM functor_id compfid. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib ifail_lib istate_lib