proposition: Lemma map_size_insert {A} i x (m : M A) : size (<[i:=x]> m) = (match m !! i with Some _ => id | None => S end) (size m).
proof: Proof. destruct (m !! i) as [y|] eqn:?; simpl. - rewrite <-(insert_id m i y) at 2 by done. rewrite <-!(insert_delete_insert m). rewrite <-!map_to_list_length. by rewrite !map_to_list_insert by (by rewrite lookup_delete). - by rewrite <-!map_to_list_length, map_to_list_insert. Qed.
imports: Coq(Permutation) stdpp(options)