proposition: Lemma splits_guard_subseq (A : eqType) (s : seq A) : splits s = splits s >>= (fun x => guard [&& subseq x.1 s, subseq x.2 s & perm_eq (x.1 ++ x.2) s] >> Ret x) :> M _.
proof: Proof. have [n ns] := ubnP (size s); elim: n s ns => // n ih s ns. move: s ns => [ns |h t]. by rewrite bindretf perm_refl guardT bindskipf. rewrite [in X in X -> _]/= ltnS => ns. rewrite [in LHS]/= [splits (h :: t)]/= bindA. rewrite ih // [in LHS]bindA [in RHS]bindA; bind_ext => -[a b]. rewrite [subseq]lock /= -lock. rewrite [in LHS]bindA [in RHS]bindA. apply: bind_ext_guard => /and3P[ta tb abt]; rewrite [subseq]lock /= -lock. rewrite !bindretf alt_bindDl !bindretf; congr (_ [~] _). rewrite [subseq (_ :: _) _]/= eqxx ta andTb perm_cons abt andbT. by rewrite (subseq_trans tb (subseq_cons _ _)) guardT bindskipf. rewrite (subseq_trans ta (subseq_cons _ _)) andTb. rewrite [subseq (_ :: _) _]/= eqxx tb andTb. rewrite -cat_rcons -cats1 -catA perm_catCA perm_cons abt. by rewrite guardT bindskipf. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib Equations(Equations)