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