fact: Definition shift : forall A : UU0, ((A -> M r) -> M r) -> M A := fun A h => fun c => h (fun v c' => c' (c v)) ssrfun.id.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib ifail_lib istate_lib itrace_lib imonad_transformer