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