proposition: Lemma splits_bseqE s : splits s = fmap (fun '(ys, zs) => (bseqval ys, bseqval zs)) (splits_bseq s) :> M _.
proof: Proof. elim: s => /= [|h t ih]; first by rewrite fmapE bindretf. rewrite {}ih /= !fmapE 2!bindA; bind_ext => -[a b] /=. by rewrite bindretf alt_bindDl 2!bindretf. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib Equations(Equations)