proposition: Lemma uunitbP5 x : reflect (x = Unit) (uunitb x).
proof: Proof. rewrite /uunitb !pcmE; case: x=>x1 x2 x3 x4 x5 /=. do ![case: unitbP=>[->|H] /=; last by constructor; case]. by constructor. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq bigop fintype finset) pcm(options axioms prelude seqperm pred seqext)