proposition: Lemma xsep_eq x y pfx pfy : x = y -> @ex_sep x pfx = @ex_sep y pfy.
proof: Proof. by move=>E; subst y; congr ex_sep; apply: pf_irr. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)