proposition: Lemma sepit_perm s1 s2 (f : A -> Pred U) : perm s1 s2 -> sepit s1 f =p sepit s2 f.
proof: Proof. elim: s1 s2 =>[|x s1 IH] s2 /=; first by move/pperm_nil=>->. move=>H; have Hx: x \In s2 by apply/(pperm_in H)/In_cons; left. case: (In_split Hx)=>s21[s22] E; rewrite {s2 Hx}E in H *. move/pperm_cons_cat_cons: H=>/IH {}IH. rewrite sepit_cons sepit_cat /= =>h; split. - case=>h1[h2][{h}-> H1]; rewrite IH sepit_cat. case=>_[_][{h2}-> [hs3][E3 -> H3] [hs4][E4 -> H4]]; rewrite joinCA. exists (seqjoin hs3), (h1 \+ seqjoin hs4); split=>//; first by exists hs3. by rewrite sepit_cons; exists h1, (seqjoin hs4); split=>//; exists hs4. case=>_[h2][{h}-> [hs1][Hs1 -> H1]]; rewrite sepit_cons. case=>h3[_][{h2}-> H3 [hs2][Hs2 -> H2]]; rewrite joinCA. exists h3, (seqjoin hs1 \+ seqjoin hs2); split=>//. rewrite IH; exists (hs1 ++ hs2); split. - by rewrite !size_cat Hs1 Hs2. - by rewrite /seqjoin big_cat. by rewrite zip_cat //; apply/All_cat. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq bigop fintype finset) pcm(options axioms prelude seqperm pred seqext)