proposition: Lemma map_size_list_to_map {A} (l : list (K * A)) : NoDup l.*1 → size (list_to_map l : M A) = length l.
proof: Proof. induction l; csimpl; inv 1; simplify_eq/=; [by rewrite map_size_empty|]. rewrite map_size_insert_None by eauto using not_elem_of_list_to_map_1. eauto with f_equal. Qed.
imports: Coq(Permutation) stdpp(options)