proposition: Lemma fmap_if (A B : UU0) (f : A -> B) b (m : M A) a : fmap f (if b then m else Ret a) = if b then fmap f m else Ret (f a).
proof: Proof. case: ifPn => Hb //; by rewrite fmapE bindretf. Qed.
imports: ssrmatching JMeq mathcomp(all_ssreflect) imonae_lib HB(structures)