proposition: Lemma splits_isNondet A (s : seq A) : plus_isNondet (splits s : M _).
proof: Proof. elim: s => [|h t ih /=]; first by exists (ndRet ([::], [::])). have [syn syn_splits] := ih. exists (ndBind syn (fun '(a, b) => ndAlt (ndRet (h :: a, b)) (ndRet (a, h :: b)))). by rewrite /= syn_splits; bind_ext => -[]. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib Equations(Equations)