proposition: Lemma snd_morph_ax : morph_axiom (@sepT (prodPCM U1 U2)) snd.
proof: Proof. by split=>[|x y]; rewrite ?pcmPE //= =>/andP []. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)