proposition: Lemma mutex_eqP : Equality.axiom mutex_eq.
proof: Proof. case=>[||x]; case=>[||y] /=; try by constructor. by case: eqP=>[->|H]; constructor=>//; case=>/H. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options prelude pred) pcm(pcm morphism natmap)