proposition: Lemma guard_splits {T A : UU0} (p : pred T) (t : seq T) (f : seq T * seq T -> M A) : splits t >>= (fun x => guard (all p t) >> f x) = splits t >>= (fun x => guard (all p x.1) >> guard (all p x.2) >> f x).
proof: Proof. rewrite -plus_commute//. elim: t => [|h t ih] in p f *; first by rewrite 2!bindretf guardT bindmskip. rewrite [LHS]/= guard_and 2!bindA ih /= plus_commute//. rewrite bindA; bind_ext => -[a b] /=. rewrite !alt_bindDl !bindretf /= !guard_and !bindA !alt_bindDr. by congr (_ [~] _); rewrite plus_commute. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib Equations(Equations)