proposition: Lemma map_lookup_zip_Some {A B} (m1 : M A) (m2 : M B) i p : map_zip m1 m2 !! i = Some p ↔ m1 !! i = Some p.1 ∧ m2 !! i = Some p.2.
proof: Proof. rewrite map_lookup_zip_with_Some. destruct p. naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)