proposition: Lemma algebraic_flush : algebraicity flush_op.
proof: Proof. move=> A B f [x w]. rewrite output_bindE. rewrite /flush_op /=. rewrite /flush /=. rewrite /actm /=. rewrite output_bindE. case: f => x' w'. Abort. End outputops. Module Output'. Section output. Variable L : UU0. Local Notation M := (OutputMonad.acto L). Definition output : seq L -> M unit := fun w => output_op _ _ (w, Ret tt). Lemma outputE : output = fun w => (tt, w). Proof. apply funext => w. by rewrite /output /= /imonad_model.output /= cats0. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib ifail_lib istate_lib itrace_lib imonad_transformer