proposition: Lemma fprod_morph_ax : morph_axiom (sep_prod D1 D2) (f1 \* f2).
proof: Proof. rewrite /fprod; split=>[|x y]; first by rewrite !pfunit. by case/andP=>/= W1 W2 /andP [H1 H2]; rewrite !pfV2 /= ?(pfjoin,W1,W2). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)