proposition: Lemma sepitT1 x f : sepit setT f =p f x # sepit (setT :\ x) f.
proof: Proof. by rewrite (sepitS x) in_setT. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq bigop fintype finset) pcm(options axioms prelude seqperm pred seqext)