proposition: Lemma map_Exists_to_list m : map_Exists P m ↔ Exists (uncurry P) (map_to_list m).
proof: Proof. rewrite Exists_exists. split. - intros [? [? [? ?]]]. eexists (_, _). by rewrite elem_of_map_to_list. - intros [[??] [??]]. eexists _, _. by rewrite <-elem_of_map_to_list. Qed.
imports: Coq(Permutation) stdpp(options)