proposition: Lemma setI_s2 x y: nonempty y -> (forall i, inc i y -> sub x i) -> sub x (intersection y).
proof: Proof. by move=> ne hyp t tx; apply:(setI_i ne) => v /hyp; apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)