proposition: Lemma algebraic_local : algebraicity local_op.
proof: Proof. move=> A B f t. rewrite environment_bindE. rewrite /local_op /=. rewrite /local /=. rewrite /actm /=. case: t => /= ee m. rewrite environment_bindE. apply funext=> x /=. Abort. End environmentops. Module Environment. Section environment. Variable E : UU0. Local Notation M := (EnvironmentMonad.acto E). Definition ask : M E := ask_op _ _ Ret. Lemma askE : ask = fun e => e. Proof. by []. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib ifail_lib istate_lib itrace_lib imonad_transformer