proposition: Lemma sepI_sepax : seprel_axiom (sepI X Y).
proof: Proof. case: pfx pfy=>X0 Xc Xu Xa [Y0 Yc Yu Ya]. rewrite /sepI; split=>[|x y|x y|x y z]. - by rewrite X0 Y0. - by move=>D; rewrite Xc // Yc. - by move=>D /andP [/Xu -> // /Yu ->]. move=>D /andP [X1 Y1] /andP [X2 Y2]. case/andP: (Xa x y z D X1 X2)=>->->. by case/andP: (Ya x y z D Y1 Y2)=>->->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)