proposition: Lemma map_lookup_zip_with_Some {A B C} (f : A → B → C) (m1 : M A) (m2 : M B) i z : map_zip_with f m1 m2 !! i = Some z ↔ ∃ x y, z = f x y ∧ m1 !! i = Some x ∧ m2 !! i = Some y.
proof: Proof. rewrite map_lookup_zip_with. destruct (m1 !! i), (m2 !! i); naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)