proposition: Lemma unitb (x : mutex) : reflect (x = Unit) (if x is nown then true else false).
proof: Proof. by case: x=>[||x]; constructor; rewrite !pcmE. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options prelude pred) pcm(pcm morphism natmap)