proposition: Lemma joinmK (m1 m2 m : mutexPCM) : valid (m1 \+ m) -> m1 \+ m = m2 \+ m -> m1 = m2.
proof: Proof. by case: m m1 m2=>[||m][||m1][||m2]; rewrite !pcmE. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options prelude pred) pcm(pcm morphism natmap)