proposition: Lemma inv_cprod (U1 U2 V1 V2 : pcm) (D1 : sep_rel U1) (D2 : sep_rel U2) (f : morphism V1 D1) (g : morphism V2 D2) : inv_morph f -> inv_morph g -> inv_morph [morphism of f \* g].
proof: Proof. case=>HD1 Hf [HD2 Hg]; split=>[a1 a2 a'|]; rewrite /sep_prod /=. - case/andP=>Va Vb /andP [/(HD1 _ _ _ Va) H1 /(HD2 _ _ _ Vb) H2]. by case/andP=>/H1 /andP [->->] /H2 /andP [->->]. move=>/= a1 b1 b2 /andP [Va Vb] /andP [H1 H2][]. case/(Hf _ _ _ Va H1)=>c1 [c2][E1 Vc1 Y1 Fc1 Fc2]. case/(Hg _ _ _ Vb H2)=>d1 [d2][E2 Vd1 Y2 Fd1 Fd2]. exists (c1, d1), (c2, d2); rewrite /fprod /= Vc1 Vd1. by rewrite Fc1 Fc2 Fd1 Fd2 Y1 Y2 pcmPE -E1 -E2 -!prod_eta. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype) pcm(options axioms prelude) pcm(pcm morphism)