proposition: Lemma foldr_insert_union {A} (m : M A) l : foldr (λ p, <[p.1:=p.2]>) m l = list_to_map l ∪ m.
proof: Proof. induction l as [|i l IH]; simpl; [by rewrite (left_id_L _ _)|]. by rewrite IH, insert_union_l. Qed.
imports: Coq(Permutation) stdpp(options)