proposition: Lemma sepit0 f : sepit set0 f =p emp.
proof: Proof. rewrite /sepit (IterStar.perm_sepit (s2 := filter pred0 (enum I))). - by rewrite filter_pred0 IterStar.sepit0. apply: uniq_perm; first by exact: enum_uniq. - by rewrite filter_uniq // enum_uniq. by move=>x; rewrite !mem_filter /= in_set0. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq bigop fintype finset) pcm(options axioms prelude seqperm pred seqext)