proposition: Lemma sublocal_pvalI : sublocal_rel P cond D -> local_rel (fun x y => P (pval x) (pval y)) (fun x => cond (pval x)).
proof: Proof. move=>L p x y /[dup] C /pf_cond; rewrite valid_pval=>W. move: (validL W) (validAR W)=>W1 W2; rewrite !pfjoin //; apply: L. - by rewrite -!pfjoin. - by apply: valid_sep2P. by rewrite -pfjoin //; apply: valid_sep2P. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)