proposition: Lemma map_Forall_to_list m : map_Forall P m ↔ Forall (uncurry P) (map_to_list m).
proof: Proof. rewrite Forall_forall. split. - intros Hforall [i x]. rewrite elem_of_map_to_list. by apply (Hforall i x). - intros Hforall i x. rewrite <-elem_of_map_to_list. by apply (Hforall (i,x)). Qed.
imports: Coq(Permutation) stdpp(options)