proposition: Lemma fmap_fail {A B : UU0} (M : failMonad) (f : A -> B) : (M # f) fail = fail.
proof: Proof. by rewrite fmapE bindfailf. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib Equations(Equations)