proposition: Lemma setIb_alt f: fgraph f -> intersectionb f = intersection (range f).
proof: Proof. move => fgf; case: (emptyset_dichot f) => fe. by rewrite fe range_set0 setI_0 setIb_0. set_extens t. move => ti; apply:setI_i. move: fe => [w tf]; exists (Q w); apply/funI_P; ex_tac. move=> y /(range_gP fgf) [x xdf ->]; exact: (setIb_hi ti xdf). move => ti; apply:setIb_i => // i idf; apply: (setI_hi ti). apply /(range_gP fgf); ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)