proposition: Lemma skip_fmap (A B : UU0) (f : A -> B) (mb : M B) ma : mb >> (fmap f ma) = fmap f (mb >> ma).
proof: Proof. by rewrite fmap_bind fcomp_def. Qed.
imports: ssrmatching JMeq mathcomp(all_ssreflect) imonae_lib HB(structures)