proposition: Lemma lookup_union_with m1 m2 i : union_with f m1 m2 !! i = union_with f (m1 !! i) (m2 !! i).
proof: Proof. unfold union_with, map_union_with. rewrite lookup_merge. by destruct (m1 !! i), (m2 !! i). Qed.
imports: Coq(Permutation) stdpp(options)