proposition: Corollary perm_sepit s1 s2 (f : A -> Pred U) : perm_eq s1 s2 -> sepit s1 f =p sepit s2 f.
proof: Proof. by move/perm_eq_perm; exact: sepit_perm. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq bigop fintype finset) pcm(options axioms prelude seqperm pred seqext)