proposition: Lemma sep_prod_seprel_ax U1 U2 (R1 : sep_rel U1) (R2 : sep_rel U2) : seprel_axiom (sep_prod R1 R2).
proof: Proof. rewrite /sep_prod; split=>[|x y|x y|x y z]. - by rewrite !sep00. - by case/andP=>/sepC -> /sepC ->. - by case/andP=>?? /andP [/sepx0 -> // /sepx0 ->]. case/andP=>V1 V2 /andP [D1 D2] /andP [/= Z1 Z2]. by rewrite !(sepAxx V1 D1 Z1) !(sepAxx V2 D2 Z2). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)