proposition: Lemma size_dom `{!Elements K D, !FinSet K D} {A} (m : M A) : size (dom m) = size m.
proof: Proof. induction m as [|i x m ? IH] using map_ind. { by rewrite dom_empty, map_size_empty, size_empty. } assert ({[i]} ## dom m). { intros j. rewrite elem_of_dom. unfold is_Some. set_solver. } by rewrite dom_insert, size_union, size_singleton, map_size_insert_None, IH. Qed.
imports: stdpp(options)