proposition: Lemma map_to_list_empty_iff {A} (m : M A) : map_to_list m = [] ↔ m = ∅.
proof: Proof. split. - rewrite <-Permutation_nil_r, <-map_to_list_empty. apply map_to_list_inj. - intros ->. apply map_to_list_empty. Qed.
imports: Coq(Permutation) stdpp(options)