proposition: Lemma sepXEQ (U : pcm) (D1 D2 : rel U) : D1 =s D2 -> seprel_axiom D1 <-> seprel_axiom D2.
proof: Proof. by move/sepEQ=>H; rewrite !orth_sep; apply: orthXEQ. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)