proposition: Lemma pmorph_morph_ax : morph_axiom (sepI D1 D2) (f1 \** f2).
proof: Proof. split=>[|x y] /=; first by rewrite !pcmPE !pfunit. by move=>V /andP [S1 S2]; rewrite !pcmPE (pfV2 f1 V S1) (pfV2 f2 V S2) !pfjoin. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)