proposition: Lemma sel_morph_ax t : morph_axiom (@sepT (fin_prod_PCM Us)) (sel t).
proof: Proof. split=>[|x y /forallP V _]; first by rewrite sel_fin. split; last by rewrite sel_fin. by move: (V t); rewrite sel_fin. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)