proposition: Lemma finI_from1 (I : choiceType) T (D : set I) (f : I -> set T) i : D i -> finI_from D f (f i).
proof: Proof. move=> Di; exists [fset i]%fset; first by move=> ?; rewrite !inE => /eqP ->. by rewrite bigcap_fset big_seq_fset1. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed