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