proposition: Lemma bind_if (M : monad) (A B : UU0) (b : bool) (m : M A) (f g : A -> M B) : m >>= (fun x => if b then f x else g x) = if b then m >>= f else m >>= g.
proof: Proof. by case: ifPn. Qed.
imports: ssrmatching mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy