proposition: Lemma res_morph_ax : morph_axiom (sepI S D) ('res_S f).
proof: Proof. rewrite /res; split=>[|x y]; first by rewrite sep00 pfunit. by move=>W /andP [X H]; rewrite !(sep0E W X) (sepU0 W X) pfjoin // pfV2. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)