proposition: Lemma sepjoin_seprel_ax : seprel_axiom ('sep_join f1 f2).
proof: Proof. rewrite /sep_join; split=>[|x y W|x y W|x y z W]. - by rewrite !sep00 ?unitL !pfunit ?unitL valid_unit. - by rewrite (sepC D1) // (sepC D2) // (joinC (f1 x \+ f2 x)). - case/and3P=>V1 V2; rewrite (sepx0 W V1) (sepx0 W V2) !pfunit // !unitR. by apply: validL. case/and3P=>V1 V2 Wa /and3P [W1 W2]. set j1 := (sepAxx W V1 W1); set j2 := (sepAxx W V2 W2). rewrite !pfjoin ?j1 ?j2 ?(validLE3 W) //=. rewrite !(pull (f2 y)) !joinA !(pull (f1 y)) !joinA. rewrite !(pull (f2 x)) !joinA !(pull (f1 x)) -!joinA=>Wb. by rewrite !(validRE3 Wb). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)