proposition: Lemma map_to_list_length {A} (m : M A) : length (map_to_list m) = size m.
proof: Proof. apply (map_fold_ind (λ n m, length (map_to_list m) = n)); clear m. { by rewrite map_to_list_empty. } intros i x m n ? IH. by rewrite map_to_list_insert, <-IH by done. Qed.
imports: Coq(Permutation) stdpp(options)