proposition: Lemma natunlift_morph_ax : morph_axiom (@sepT _) nat_unlift.
proof: Proof. by rewrite /nat_unlift; split=>//; case=>// x; case. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype) pcm(options prelude) pcm(pcm morphism)