proposition: Lemma cancelMx t1 t2 x : (mx t1 \+ x = mx t2) <-> (t1 = t2) * (x = Unit).
proof: Proof. by case: x=>[||x] //=; split=>//; case=>->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options prelude pred) pcm(pcm morphism natmap)