proposition: Lemma sepit0 f : sepit [::] f =p emp.
proof: Proof. move=>h; split. - by case=>/= hs [/size0nil -> -> _]; rewrite /seqjoin !big_nil. by move=>->; exists [::]; rewrite /seqjoin !big_nil. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq bigop fintype finset) pcm(options axioms prelude seqperm pred seqext)