proposition: Corollary eq_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. by move=>H; apply: sepitF=>x Hx; apply/H/mem_seqP. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq bigop fintype finset) pcm(options axioms prelude seqperm pred seqext)