proposition: Lemma setIb_hi g x i: inc x (intersectionb g) -> inc i (domain g) -> inc x (Vg g i).
proof: Proof. by move => /setIb_P pa pb; apply: pa => //; apply /domain_set0P; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)