proposition: Lemma sepEQ (U : pcm) (D1 D2 : rel U) : D1 =s D2 <-> (fun x y => valid (x \+ y) && D1 x y) =2 (fun x y => valid (x \+ y) && D2 x y).
proof: Proof. split; first by move=>S=>x y; case: (valid (x \+ y)) (S x y)=>// ->. by move=>S x y V; move: (S x y); rewrite V. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)