proposition: Lemma map_lookup_zip_with {A B C} (f : A → B → C) (m1 : M A) (m2 : M B) i : map_zip_with f m1 m2 !! i = (x ← m1 !! i; y ← m2 !! i; Some (f x y)).
proof: Proof. unfold map_zip_with. rewrite lookup_merge. by destruct (m1 !! i), (m2 !! i). Qed.
imports: Coq(Permutation) stdpp(options)