proposition: Lemma list_to_map_app {A} (l1 l2 : list (K * A)): list_to_map (l1 ++ l2) =@{M A} list_to_map l1 ∪ list_to_map l2.
proof: Proof. induction l1 as [|[??] ? IH]; simpl. { by rewrite (left_id _ _). } by rewrite IH, insert_union_l. Qed.
imports: Coq(Permutation) stdpp(options)