proposition: Lemma sublocal_psubE : sublocal_rel (fun x y => P (psub U x) (psub U y)) (fun x => cond (psub U x)) D -> local_rel P cond.
proof: Proof. have pf s : cond (psub U s) -> valid s by move/pf_cond/valid_psub1. move/(sublocal_pvalI (U:=U) pf)=>L p x y C H. by move: (L p x y); rewrite !psub_pval; apply. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)