proposition: Lemma sepitF (s : {set I}) f1 f2 : (forall x, x \in s -> f1 x =p f2 x) -> sepit s f1 =p sepit s f2.
proof: Proof. move=>H; apply: IterStar.eq_sepitF=>x H1; apply: H. by rewrite -mem_enum. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq bigop fintype finset) pcm(options axioms prelude seqperm pred seqext)