proposition: Lemma setIf_P I f: nonempty I -> forall x, (inc x (intersectionf I f) <-> (forall j, inc j I -> inc x (f j))).
proof: Proof. move => h x; split; first by move/(setIt_P _ h) => aux j [ji <-]; apply: aux. move => aux; apply/(setIt_P _ h) => j; apply: aux; apply: R_inc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)