proposition: Lemma sepitF s (f1 f2 : A -> Pred U) : (forall x, x \In s -> f1 x =p f2 x) -> sepit s f1 =p sepit s f2.
proof: Proof. elim: s=>[|x s IH] H h; first by rewrite !sepit0. have /IH {IH}H': forall x : A, x \In s -> f1 x =p f2 x. by move=>? H0; apply: H; apply/In_cons; right. have Hx : x \In x :: s by apply/In_cons; left. by rewrite !sepit_cons; split; case=>h1[h2][{h}-> H1 H2]; exists h1, h2; split=>//; [rewrite -H | rewrite -H' | rewrite H | rewrite H']. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq bigop fintype finset) pcm(options axioms prelude seqperm pred seqext)