proposition: Lemma map_img_finite m : set_finite (map_img m).
proof: Proof. induction m as [|i x m ? IH] using map_ind. - rewrite map_img_empty. apply empty_finite. - eapply set_finite_subseteq; [by apply map_img_insert_subseteq|]. apply union_finite; [apply singleton_finite | apply IH]. Qed.
imports: Coq(Permutation) stdpp(options)