proposition: Lemma mxundef_ax T : morph_axiom (@sep_mxundef T) (@mxundef T).
proof: Proof. by split=>//; case=>[||x] // [||[]] //; case: x. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options prelude pred) pcm(pcm morphism natmap)