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