proposition: Lemma mxE5 t1 t2 x : (((mx t1 \+ x == mx t2) = (t1 == t2) && (x == Unit)) * ((x \+ mx t1 == mx t2) = (t1 == t2) && (x == Unit))) * (((mx t1 == mx t2 \+ x) = (t1 == t2) && (x == Unit)) * ((mx t1 == x \+ mx t2) = (t1 == t2) && (x == Unit))).
proof: Proof. have L : forall t1 t2 x, (mx t1 \+ x == mx t2) = (t1 == t2) && (x == Unit). - by move=>*; apply/eqP/andP=>[/cancelMx[]->->|[]/eqP->/eqP->]. by do !split=>//; rewrite ?L // eq_sym L eq_sym. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options prelude pred) pcm(pcm morphism natmap)