fact: Definition xgseprel_axiom := [/\ forall k x y, valid (x \+ y) -> P k (x \+ y) <-> P k x \/ P k y, forall k1 k2 x y, valid (x \+ y) -> P k1 x -> P k2 y -> k1 <> k2, forall k1 k2 x y z, valid (x \+ y \+ z) -> P k1 x -> Q k1 x y -> Q k2 (x \+ y) z -> k1 = k2, forall k1 k2 x y z, valid (x \+ y \+ z) -> P k1 x -> Q k1 x (y \+ z) -> P k2 y-> Q k2 y (x \+ z) -> k1 = k2, forall k, P k Unit -> Q k Unit Unit, forall k x y, valid (x \+ y) -> P k x -> Q k x y -> Q k x Unit, forall k y, valid y -> P k Unit -> Q k Unit y, forall k x y z, valid (x \+ y \+ z) -> P k x -> (forall k', ~ P k' y) -> Q k x y -> Q k (x \+ y) z -> Q k x (y \+ z) & forall k x y z, valid (x \+ y \+ z) -> P k x -> (forall k', ~ P k' y) -> Q k x (y \+ z) -> Q k x y /\ Q k (x \+ y) z].
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)