fact: Definition catch {A : UU0} (m1 m2 : failPState A) := fun s => match m1 s with | (Some a, s') => (Some a, s') | (None, s') => m2 s' end.
imports: mathcomp(all_ssreflect) monae_lib hierarchy monad_lib fail_lib state_lib monad_transformer