proposition: Lemma psiK (op : E ~> M) : phi (psi op) = op.
proof: Proof. apply/nattrans_ext => A. rewrite phiE /= psiE; apply: boolp.funext => m /=. rewrite -(compE (op _)) -(natural op) -(compE Join). by rewrite compA joinMret. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib fail_lib state_lib