proposition: Lemma setIb_rewrite f g: fgraph f -> range f = domain g -> intersectionb g = intersectionb (g \cf f).
proof: Proof. move=> fgf rfdg. case: (emptyset_dichot g) => gp. symmetry;congr intersectionb; rewrite gp; apply /set0_P=> t /funI_P [z zd _]. have :(inc (Vg f z) (range f)) by fprops. rewrite rfdg gp domain_set0; apply: in_set0. have nec: (nonempty (g \cf f)). move: gp => [x xg]. have : (inc (P x) (range f)) by rewrite rfdg; fprops. move/(range_gP fgf) => [y ydf etc]. exists (J y (Vg g (Vg f y))); apply/funI_P; ex_tac. set_extens t. move/(setIb_P gp) => h; apply/(setIb_P nec); rewrite /composef; aw => j jdf. rewrite LgV //; apply: h; rewrite - rfdg; apply range_gP => //; ex_tac. move/(setIb_P nec) => h; apply/(setIb_P gp) => i; rewrite -rfdg. move/(range_gP fgf) => [x xdf ->]; move: (h x);rewrite Lgd LgV //. by apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)