proposition: Lemma liftM2_isNondet A B C (f : A -> B -> C) (ma : M A) (mb : M B) : plus_isNondet ma -> plus_isNondet mb -> plus_isNondet (liftM2 f ma mb).
proof: Proof. move=> [s1 s1_ma] [s2 s2_mb]. exists (ndBind s1 (fun a => ndBind s2 (fun b => ndRet (f a b)))). by rewrite /= s1_ma /comp /= s2_mb. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib Equations(Equations)