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