proposition: Lemma dsplitsE (A : UU0) (s : seq A) : splits s = fmap (fun x => (dsplitsT1 x, dsplitsT2 x)) (dsplits s) :> M _.
proof: Proof. rewrite fmapE /dsplits /= bindA [LHS]splits_guard; bind_ext => -[a b]. rewrite /dassert; case: Bool.bool_dec => /= [|/negP] abs. by rewrite !bindretf /= abs guardT bindskipf. by rewrite (negbTE abs) guardF 2!bindfailf. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib Equations(Equations)