proposition: Lemma sepitS x (s : {set I}) f : sepit s f =p if x \in s then f x # sepit (s :\ x) f else sepit s f.
proof: Proof. case E: (x \in s)=>//. rewrite (IterStar.sepitP x (s:=enum s) f (enum_uniq s)) mem_enum E. have Hp: perm_eq [seq y <- enum s | predC1 x y] (enum (s :\ x)). - rewrite -filter_predI. apply: uniq_perm=>[||y]; try by rewrite enum_uniq. by rewrite !mem_filter /= in_setD1. by move=>h0; split; case=>h1[h2][{h0}-> H1 H]; exists h1, h2; split=>//; rewrite IterStar.perm_sepit; try by [exact: H]; [rewrite perm_sym |]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq bigop fintype finset) pcm(options axioms prelude seqperm pred seqext)