proposition: Lemma mxE2 t : (((mx t == nown) = false) * ((nown == mx t) = false)) * (((mx t == mx_undef) = false) * ((mx_undef == mx t) = false)).
proof: Proof. by []. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options prelude pred) pcm(pcm morphism natmap)