proposition: Lemma sep0_seprel_ax (U : tpcm) : seprel_axiom (@sep0 U).
proof: Proof. rewrite /sep0; split=>[|x y|x y|x y z]. - by rewrite tpcmE. - by rewrite andbC. - by move=>V /andP [->]; rewrite tpcmE. move=>V /andP [/unitbP -> /unitbP ->] /andP [_ /unitbP ->]. by rewrite unitL !tpcmE. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)