proposition: Lemma distrib_prod_inter2_prod f g: fgraph f -> fgraph g -> domain f = domain g -> (productb f) \cap (productb g) = productf (domain f) (fun i => (Vg f i) \cap (Vg g i)).
proof: Proof. move=> ff fg dfdg; set_extens x. move=> /setI2_P [] /setXb_P [fx dx vx] /setXb_P [ _ dx' vx']. apply /setXf_P;split => // i id. by apply: setI2_i; [apply: vx | apply: vx'; ue]. move /setXf_P=> [fx dx vx]; apply: setI2_i. by apply /setXb_P;split => // i idf; case /setI2_P: (vx _ idf). by apply /setXb_P; rewrite - dfdg; split => // i idf; case /setI2_P: (vx _ idf). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)