proposition: Lemma sublocal_pval : sublocal_rel P cond [eta D] <-> local_rel (fun x y => P (pval x) (pval y)) (fun x => cond (pval x)).
proof: Proof. split; first by apply: sublocal_pvalI. move=>L p x y C Sxp Sy H; move: (pf_cond C)=>W. move: (validL W) (validAR W) (validR W)=>W1 W2 W3; move: (validL W1)=>Wx. have Spy : D p y by rewrite (sepAxx _ Sxp Sy). suff : P (pval (psub U x \+ psub U p)) (pval (psub U y)). - by rewrite -pfjoin ?(pval_psub,sep0E _ Spy,sep0E _ Sy). apply: L; first by rewrite -!pfjoin // pval_psub ?(sepU0 W Sy). by rewrite -pfjoin ?(pval_psub,sepU0 _ Spy,sep0E _ Sxp). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)