proposition: Lemma setIf_alt I f: (intersectionf I f = intersection (range (Lg I f))).
proof: Proof. rewrite - setIb_alt; fprops; rewrite /intersectionb; aw. apply:setIf_exten => i iI; rewrite LgV//. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)