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