proposition: Lemma mxE0 x y : x \+ y = Unit -> (x = Unit) * (y = Unit).
proof: Proof. exact: GeneralizedMutex.join0E. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options prelude pred) pcm(pcm morphism natmap)