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