proposition: Theorem distrib_inter_prod f sa sb: (nonempty sa \/ nonempty sb) -> intersectionf sb (fun k => productf sa (fun i=> Vg f (J i k))) = productf sa (fun i => intersectionf sb (fun k=> Vg f (J i k))).
proof: Proof. move=> aux ; set_extens x => xi. case: (emptyset_dichot sb) => nb. by move: xi; rewrite nb setIf_0 => /in_set0. move: (nb)=> [y yb]; move /setXf_P: (setIf_hi xi yb) => [fx dx px]. apply /setXf_P;split=> // i id; apply: (setIf_i nb). by move => j jsb; move: (setIf_hi xi jsb) => /setXf_P [_ _]; apply. move /setXf_P: xi => [fx dx px]. case: (emptyset_dichot sb) => nsb. case: aux; last by rewrite nsb; case /nonemptyP. by move => [t ta]; move: (px _ ta); rewrite nsb setIf_0 => /in_set0. apply: (setIf_i nsb) => j jsb; apply/ setXf_P;split => // i id. move: (px _ id)=> xi; apply: (setIf_hi xi jsb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)