proposition: Lemma uunitbP_fin x : reflect (x = Unit) (uunitb x).
proof: Proof. case H : (uunitb x); constructor. - move/forallP: H=>H; apply: fin_ext=>a. by rewrite sel_fin; move/unitbP: (H a). move=>E; move/negP: H; apply; apply/forallP=>t. by rewrite E sel_fin unitb0. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq bigop fintype finset) pcm(options axioms prelude seqperm pred seqext)