proposition: Lemma opt_unitbP (x : optPCM U) : reflect (x = Unit) (opt_unitb x).
proof: Proof. case: x=>/= [a|]. - case: eqP=>[->|E]; constructor=>// [[E']]. by rewrite E' in E. by constructor. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq bigop fintype finset) pcm(options axioms prelude seqperm pred seqext)