fact: Definition prl_ne2_sigma := Zo (productb FS_fam) (fun A => (forall i, inc i (psI S) -> nonempty (Vg A i)) /\ (forall i j, gle (psr S) i j -> sub (Vfs (Vg (psf S) (J i j)) (Vg A j)) (Vg A i))).
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)