proposition: Lemma guard_all_qperm {T B : UU0} (p : pred T) s (f : seq T -> M B) : qperm s >>= (fun x => guard (all p s) >> f x) = qperm s >>= (fun x => guard (all p x) >> f x).
proof: Proof. rewrite -plus_commute//. have [n leMn] := ubnP (size s); elim: n => // n ih in s f leMn *. case: s leMn => [|h t]; first by move=> _; rewrite qperm_nil !bindretf. rewrite ltnS => tn. rewrite qperm_cons !bindA /= guard_and bindA (@plus_commute _ _ (guard (all p t)))//. rewrite guard_splits splits_bseqE fmapE 2!bindA plus_commute//. bind_ext => -[a b]; rewrite 2!bindretf !bindA /=. rewrite (@plus_commute _ _ (guard (all p b)))//. rewrite ih; last by rewrite (leq_trans _ tn) //= ltnS size_bseq. rewrite (@plus_commute _ _(guard (p h)))//. bind_ext => a'; rewrite !bindA (@plus_commute _ _ (guard (p h)))//. rewrite ih; last by rewrite (leq_trans _ tn) //= ltnS size_bseq. rewrite (@plus_commute _ _ (guard (p h)))// plus_commute//. bind_ext => b'; rewrite !bindretf all_cat /= andbA andbAC !guard_and !bindA. by under eq_bind do rewrite plus_commute//. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib Equations(Equations)