proposition: Theorem setIf_A L f g: (alls L (fun i => (nonempty (g i)))) -> intersectionf (unionf L g) f = intersectionf L (fun l => intersectionf (g l) f).
proof: Proof. move=> neall. case: (emptyset_dichot L) => sgp;first by rewrite sgp setUf_0 // 2! setIf_0. have neu: (nonempty (unionf L g)). by move: sgp=> [x xsg]; move: (neall _ xsg)=> [y iy]; exists y; union_tac. set_extens t. move/(setIf_P _ neu) => h; apply: (setIf_i sgp) => j jsg. apply: (setIf_i (neall _ jsg)) => k kj; apply: h; union_tac. move/(setIf_P _ sgp) => h; apply: (setIf_i neu) => j /setUf_P [y ysg jgy]. exact (setIf_hi (h _ ysg) jgy). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)