fact: Definition Restart A B (r : W A) (f : M B) : W B := if r is inr (_, env) then f env else inl tt.
imports: JMeq mathcomp(all_ssreflect finmap) monae_lib HB(structures) hierarchy monad_lib fail_lib state_lib trace_lib monad_transformer monad_model