proposition: Lemma map_img_alt m : map_img m ≡ list_to_set (map_to_list m).*2.
proof: Proof. induction m as [|i x m ? IH] using map_ind. { by rewrite map_img_empty, map_to_list_empty. } by rewrite map_img_insert_notin, map_to_list_insert by done. Qed.
imports: Coq(Permutation) stdpp(options)