proposition: Lemma setIb_P g: nonempty g -> forall x, (inc x (intersectionb g) <-> (forall i, inc i (domain g) -> inc x (Vg g i))).
proof: Proof. move/domain_set0P => h x; exact: (setIf_P _ h). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)