proposition: Theorem iim_fun_setIf I f g: function g -> (Vfi g (intersectionf I f)) = (intersectionf I (fun i => Vfi g (f i))).
proof: Proof. move=> fg. apply: extensionality; first by rewrite iim_fun_pr; apply:dirim_setIf. case: (emptyset_dichot I) => ie; first by rewrite ie setIf_0 ; fprops. move => t /(setIf_P _ ie) aj. move: (ie)=> [x xI]; move: (aj _ xI) => /iim_fun_P[u ufz Jg]. apply/iim_fun_P; ex_tac; apply: (setIf_i ie) => v /aj. move => /iim_graph_P [u' ufx Jg']. by rewrite (Vf_pr fg Jg); rewrite - (Vf_pr fg Jg'). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)