proposition: Lemma preim_seprel_ax : seprel_axiom ('preim f R).
proof: Proof. rewrite /preim; split=>[|x y|x y|x y z]; first by rewrite !pfunit !sep00. - move=>H; rewrite sepC //=; case S: (D y x)=>//=. by rewrite -sepC // pfV2 // joinC. - move=>H /andP [H1 H2]. by rewrite !pfunit (sep0E H H1) (sep0E _ H2) // pfV2. move=>H /andP [G1 F1] /andP [G2 F2]. rewrite pfjoin ?(validLE3 H) // in F2. rewrite pfjoin ?(validLE3 H) ?(sepAxx H G1 G2) //=. move: (pfVf f H G2); rewrite pfjoin ?(validLE3 H) // => D2. by rewrite !(sepAxx D2 F1 F2). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)