proposition: Lemma algebraic_output : algebraicity output_op.
proof: Proof. move=> A B f [w [x w']]. rewrite output_bindE/=. rewrite /output /=. rewrite output_bindE. by case: f => x' w''; rewrite catA. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib ifail_lib istate_lib itrace_lib imonad_transformer